theorem Matroid.IsFlat.eq_ground_of_spanning {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) (h : M.Spanning F) : F = M.E

theorem Matroid.IsFlat.spanning_iff {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : M.Spanning F ↔ F = M.E

theorem Matroid.IsFlat.inter {α : Type u_1} {M : Matroid α} {F₁ F₂ : Set α} (hF₁ : M.IsFlat F₁) (hF₂ : M.IsFlat F₂) : M.IsFlat (F₁ ∩ F₂)

theorem Matroid.isFlat_iff_closure_subset {α : Type u_1} {M : Matroid α} {F : Set α} (hF : F ⊆ M.E := by aesop_mat) : M.IsFlat F ↔ M.closure F ⊆ F

theorem Matroid.IsFlat.iInter_inter_ground {α : Type u_1} {M : Matroid α} {ι : Type u_2} {Fs : ι → Set α} (hFs : ∀ (i : ι), M.IsFlat (Fs i)) : M.IsFlat ((⋂ (i : ι), Fs i) ∩ M.E)

The intersection of an arbitrary collection of flats with the ground set is a flat. Matroid.IsFlat.iInter is often more convenient, but this works when the collection is empty.

theorem Matroid.IsFlat.biInter {α : Type u_1} {M : Matroid α} {ι : Type u_2} {Fs : ι → Set α} {s : Set ι} (hs : s.Nonempty) (hFs : ∀ i ∈ s, M.IsFlat (Fs i)) : M.IsFlat (⋂ i ∈ s, Fs i)

theorem Matroid.IsFlat.biInter_inter_ground {α : Type u_1} {M : Matroid α} {ι : Type u_2} {Fs : ι → Set α} {s : Set ι} (hFs : ∀ i ∈ s, M.IsFlat (Fs i)) : M.IsFlat ((⋂ i ∈ s, Fs i) ∩ M.E)

theorem Matroid.IsFlat.sInter {α : Type u_1} {M : Matroid α} {Fs : Set (Set α)} (hF : Fs.Nonempty) (h : ∀ F ∈ Fs, M.IsFlat F) : M.IsFlat (⋂₀ Fs)

theorem Matroid.IsFlat.sInter_inter_ground {α : Type u_1} {M : Matroid α} {Fs : Set (Set α)} (h : ∀ F ∈ Fs, M.IsFlat F) : M.IsFlat (⋂₀ Fs ∩ M.E)

@[simp]

theorem Matroid.closure_isFlat {α : Type u_1} (M : Matroid α) (X : Set α) : M.IsFlat (M.closure X)

theorem Matroid.isFlat_iff_closure_self {α : Type u_1} {M : Matroid α} {F : Set α} : M.IsFlat F ↔ M.closure F = F

theorem Matroid.isFlat_iff_subset_closure_self {α : Type u_1} {M : Matroid α} {F : Set α} (hF : F ⊆ M.E := by aesop_mat) : M.IsFlat F ↔ M.closure F ⊆ F

theorem Matroid.IsFlat.closure_subset_of_subset {α : Type u_1} {M : Matroid α} {F X : Set α} (hF : M.IsFlat F) (h : X ⊆ F) : M.closure X ⊆ F

@[simp]

theorem Matroid.IsFlat.closure_subset_iff_subset {α : Type u_1} {M : Matroid α} {F X : Set α} (hF : M.IsFlat F) (hX : X ⊆ M.E := by aesop_mat) : M.closure X ⊆ F ↔ X ⊆ F

theorem Matroid.exists_mem_closure_notMem_of_not_isFlat {α : Type u_1} {M : Matroid α} {F : Set α} (h : ¬M.IsFlat F) (hF : F ⊆ M.E := by aesop_mat) : ∃ (e : α), e ∈ M.closure F \ F

theorem Matroid.IsFlat.ssubset_closure_insert {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} (hF : M.IsFlat F) (heF : e ∉ F) (he : e ∈ M.E := by aesop_mat) : F ⊂ M.closure (insert e F)

theorem Matroid.isFlat_iff_ssubset_closure_insert_forall {α : Type u_1} {M : Matroid α} {F : Set α} (hF : F ⊆ M.E := by aesop_mat) : M.IsFlat F ↔ ∀ e ∈ M.E \ F, M.closure F ⊂ M.closure (insert e F)

theorem Matroid.isFlat_iff_forall_isCircuit' {α : Type u_1} {M : Matroid α} {F : Set α} : M.IsFlat F ↔ (∀ (C : Set α) (e : α), M.IsCircuit C → e ∈ C → C ⊆ insert e F → e ∈ F) ∧ F ⊆ M.E

theorem Matroid.isFlat_iff_forall_isCircuit {α : Type u_1} {M : Matroid α} {F : Set α} (hF : F ⊆ M.E := by aesop_mat) : M.IsFlat F ↔ ∀ (C : Set α) (e : α), M.IsCircuit C → e ∈ C → C ⊆ insert e F → e ∈ F

theorem Matroid.IsFlat.closure_exchange {α : Type u_1} {M : Matroid α} {F : Set α} {e f : α} (hF : M.IsFlat F) (he : e ∈ M.closure (insert f F) \ F) : f ∈ M.closure (insert e F) \ F

theorem Matroid.IsFlat.closure_insert_eq_closure_insert_of_mem {α : Type u_1} {M : Matroid α} {F : Set α} {e f : α} (hF : M.IsFlat F) (he : e ∈ M.closure (insert f F) \ F) : M.closure (insert e F) = M.closure (insert f F)

theorem Matroid.IsFlat.insert_indep_of_isBasis {α : Type u_1} {M : Matroid α} {I F : Set α} {e : α} (hF : M.IsFlat F) (hIF : M.IsBasis I F) (heI : e ∈ M.E \ F) : M.Indep (insert e I)

theorem Matroid.IsFlat.closure_eq_iff_isBasis_of_indep {α : Type u_1} {M : Matroid α} {I F : Set α} (hF : M.IsFlat F) (hI : M.Indep I) : M.closure I = F ↔ M.IsBasis I F

theorem Matroid.IsFlat.eq_closure_of_isBasis {α : Type u_1} {M : Matroid α} {I F : Set α} (hF : M.IsFlat F) (hI : M.IsBasis I F) : F = M.closure I

theorem Matroid.IsFlat.eRk_insert_eq_add_one {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} (hF : M.IsFlat F) (he : e ∈ M.E \ F) : M.eRk (insert e F) = M.eRk F + 1

theorem Matroid.IsFlat.rk_insert_eq_add_one {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} (hF : M.IsFlat F) (hfin : M.IsRkFinite F) (he : e ∈ M.E \ F) : M.rk (insert e F) = M.rk F + 1

theorem Matroid.IsFlat.rk_lt_of_superset {α : Type u_1} {M : Matroid α} {F X : Set α} (hF : M.IsFlat F) (hFX : F ⊂ X) (hfin : M.IsRkFinite X) (hX : X ⊆ M.E := by aesop_mat) : M.rk F < M.rk X

theorem Matroid.IsFlat.subset_of_eRelRk_eq_zero {α : Type u_1} {M : Matroid α} {F X : Set α} (hF : M.IsFlat F) (hr : M.eRelRk F X = 0) (hX : X ⊆ M.E := by aesop_mat) : X ⊆ F

theorem Matroid.IsFlat.one_le_eRelRk_of_ssubset {α : Type u_1} {M : Matroid α} {F X : Set α} (hF : M.IsFlat F) (hss : F ⊂ X) (hX : X ⊆ M.E := by aesop_mat) : 1 ≤ M.eRelRk F X

theorem Matroid.exists_insert_rk_eq_of_not_isFlat {α : Type u_1} {M : Matroid α} {F : Set α} (hFE : F ⊆ M.E) (hnF : ¬M.IsFlat F) : ∃ e ∈ M.E \ F, M.rk (insert e F) = M.rk F

theorem Matroid.IsFlat.insert_rk_eq {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} [M.RankFinite] (hF : M.IsFlat F) (he : e ∈ M.E \ F) : M.rk (insert e F) = M.rk F + 1

theorem Matroid.IsFlat.eq_of_subset_of_rk_ge {α : Type u_1} {M : Matroid α} {F F' : Set α} [M.RankFinite] (hF : M.IsFlat F) (hFF' : F ⊆ F') (hle : M.rk F' ≤ M.rk F) (hF' : F' ⊆ M.E := by aesop_mat) : F = F'

theorem Matroid.finite_setOf_isFlat {α : Type u_1} (M : Matroid α) [M.Finite] : {F : Set α | M.IsFlat F}.Finite

theorem Matroid.uniqueBaseOn_isFlat_iff {α : Type u_1} {F I E : Set α} (hIE : I ⊆ E) : (uniqueBaseOn E I).IsFlat F ↔ F ⊆ I

@[simp]

theorem Matroid.loopyOn_isFlat_iff {α : Type u_1} {F E : Set α} : (loopyOn E).IsFlat F ↔ F = E

@[simp]

theorem Matroid.emptyOn_isFlat_iff {α : Type u_1} {F : Set α} : (emptyOn α).IsFlat F ↔ F = ∅

@[simp]

theorem Matroid.freeOn_isFlat_iff {α : Type u_1} {F E : Set α} : (freeOn E).IsFlat F ↔ F ⊆ E

instance Matroid.instGroundedPredSetIsFlat : GroundedPred fun {α : Type u_2} => IsFlat

instance Matroid.instInvariantFunSetPropIsFlat : InvariantFun (fun {α : Type u_2} => IsFlat) fun {β : Type u_3} => IsFlat

theorem Matroid.isFlat_map_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) {F : Set β} : (M.map f hf).IsFlat F ↔ ∃ (F₀ : Set α), M.IsFlat F₀ ∧ F = f '' F₀

@[simp]

theorem Matroid.isFlat_mapEquiv_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} {f : α ≃ β} {F : Set β} : (M.mapEquiv f).IsFlat F ↔ M.IsFlat (⇑f ⁻¹' F)

theorem Matroid.IsFlat.map {α : Type u_1} {M : Matroid α} {F : Set α} {β : Type u_2} {f : α → β} (hF : M.IsFlat F) (hf : Set.InjOn f M.E) : (M.map f hf).IsFlat (f '' F)

theorem Matroid.IsFlat.comap {α : Type u_1} {β : Type u_2} {F : Set β} {M : Matroid β} (hF : M.IsFlat F) (f : α → β) : (M.comap f).IsFlat (f ⁻¹' F)

theorem Matroid.isFlat_comap_iff_exists {α : Type u_1} {β : Type u_2} {f : α → β} {F : Set α} {M : Matroid β} : (M.comap f).IsFlat F ↔ ∃ (F₀ : Set β), M.IsFlat F₀ ∧ F = f ⁻¹' F₀

instance Matroid.GroundedPred.instCyclic : GroundedPred fun {α : Type u_2} => Cyclic

instance Matroid.InvariantFun.instCyclic : InvariantFun (fun {α : Type u_2} => Cyclic) fun {β : Type u_3} => Cyclic

theorem Matroid.isFlat_contract {α : Type u_1} {M : Matroid α} (X C : Set α) : (M.contract C).IsFlat (M.closure (X ∪ C) \ C)

@[simp]

theorem Matroid.isFlat_contract_iff {α : Type u_1} {M : Matroid α} {F C : Set α} (hC : C ⊆ M.E := by aesop_mat) : (M.contract C).IsFlat F ↔ M.IsFlat (F ∪ C) ∧ Disjoint F C

theorem Matroid.IsFlat.union_isFlat_of_contract {α : Type u_1} {M : Matroid α} {F C : Set α} (hF : (M.contract C).IsFlat F) (hC : C ⊆ M.E := by aesop_mat) : M.IsFlat (F ∪ C)

theorem Matroid.isFlat_contract_iff' {α : Type u_1} {M : Matroid α} {F C : Set α} : (M.contract C).IsFlat F ↔ M.IsFlat (F ∪ C ∩ M.E) ∧ Disjoint F (C ∩ M.E)

theorem Matroid.IsFlat.union_isFlat_of_contract' {α : Type u_1} {M : Matroid α} {F C : Set α} (hF : (M.contract C).IsFlat F) : M.IsFlat (F ∪ M.closure C)

theorem Matroid.IsNonloop.contractElem_isFlat_iff {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} (he : M.IsNonloop e) : (M.contract {e}).IsFlat F ↔ M.IsFlat (insert e F) ∧ e ∉ F

def Matroid.isFlatContractEquiv {α : Type u_1} (M : Matroid α) (C : Set α) (hC : C ⊆ M.E := by aesop_mat) : { F : Set α // (M.contract C).IsFlat F } ≃ { F : Set α // M.IsFlat F ∧ C ⊆ F }

Flats of M ／ C are equivalent to flats of M containing C

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.isFlatContractEquiv_apply_coe {α : Type u_1} (M : Matroid α) (C : Set α) (hC : C ⊆ M.E := by aesop_mat) (F : { F : Set α // (M.contract C).IsFlat F }) : ↑((M.isFlatContractEquiv C hC) F) = ↑F ∪ C

@[simp]

theorem Matroid.isFlatContractEquiv_symm_apply_coe {α : Type u_1} (M : Matroid α) (C : Set α) (hC : C ⊆ M.E := by aesop_mat) (F : { F : Set α // M.IsFlat F ∧ C ⊆ F }) : ↑((M.isFlatContractEquiv C hC).symm F) = ↑F \ C

theorem Matroid.isFlat_restrict_iff {α : Type u_1} {M : Matroid α} {F R : Set α} (hR : R ⊆ M.E := by aesop_mat) : (M.restrict R).IsFlat F ↔ ∃ (F' : Set α), M.IsFlat F' ∧ F = F' ∩ R

theorem Matroid.isFlat_delete_iff {α : Type u_1} {M : Matroid α} {F D : Set α} : (M.delete D).IsFlat F ↔ ∃ (F' : Set α), M.IsFlat F' ∧ F = F' \ D

theorem Matroid.isFlat_delete_iff' {α : Type u_1} {M : Matroid α} {F D : Set α} : (M.delete D).IsFlat F ↔ M.closure F ⊆ F ∪ D ∧ Disjoint F D ∧ F ⊆ M.E

theorem Matroid.isFlat_restrict_iff' {α : Type u_1} {M : Matroid α} {F R : Set α} : (M.restrict R).IsFlat F ↔ F = M.closure F ∩ R ∪ R \ M.E

theorem Matroid.IsFlat.isFlat_restrict' {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) (R : Set α) : (M.restrict R).IsFlat (F ∩ R ∪ R \ M.E)

theorem Matroid.IsFlat.isFlat_restrict {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) (R : Set α) (hR : R ⊆ M.E := by aesop_mat) : (M.restrict R).IsFlat (F ∩ R)

theorem Matroid.IsFlat.closure_subset_of_isFlat_restrict {α : Type u_1} {M : Matroid α} {F R : Set α} (hF : (M.restrict R).IsFlat F) : M.closure F ⊆ F ∪ M.E \ R

theorem Matroid.IsFlat.exists_of_delete {α : Type u_1} {M : Matroid α} {F D : Set α} (hF : (M.delete D).IsFlat F) : ∃ (F₀ : Set α), M.IsFlat F₀ ∧ F = F₀ \ D

theorem Matroid.IsFlat.closure_subset_of_delete {α : Type u_1} {M : Matroid α} {F D : Set α} (hF : (M.delete D).IsFlat F) : M.closure F ⊆ F ∪ D

@[simp]

theorem Matroid.deleteElem_isFlat_iff {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} : (M.delete {e}).IsFlat F ↔ e ∉ F ∧ (M.IsFlat F ∨ M.IsFlat (insert e F))

theorem Matroid.IsFlat.contract_subset_isFlat {α : Type u_1} {M : Matroid α} {F C : Set α} (hF : M.IsFlat F) (hC : C ⊆ F) : (M.contract C).IsFlat (F \ C)

theorem Matroid.ext_isFlat {α : Type u_1} {M₁ M₂ : Matroid α} (hF : ∀ (F : Set α), M₁.IsFlat F ↔ M₂.IsFlat F) : M₁ = M₂

theorem Matroid.ext_iff_isFlat {α : Type u_1} {M₁ M₂ : Matroid α} : M₁ = M₂ ↔ ∀ (F : Set α), M₁.IsFlat F ↔ M₂.IsFlat F

theorem Matroid.IsFlat.iInter_mem_of_directed_of_isRkFinite {α : Type u_1} {M : Matroid α} {ι : Type u_2} {F : ι → Set α} (hF : ∀ (i : ι), M.IsFlat (F i)) (h_dir : Directed (fun (A B : Set α) => B ⊆ A) F) (h_fin : ∃ (i : ι), M.IsRkFinite (F i)) : ∃ (i₀ : ι), F i₀ = ⋂ (i : ι), F i

Any downwards-directed collection of flats containing a flat of finite rank must contain its intersection.

@[simp]

theorem Matroid.sigma_isFlat_iff {ι : Type u_2} {α : ι → Type u_3} {M : (i : ι) → Matroid (α i)} {F : Set ((i : ι) × α i)} : (Matroid.sigma M).IsFlat F ↔ ∀ (i : ι), (M i).IsFlat (Sigma.mk i ⁻¹' F)

@[simp]

theorem Matroid.disjointSigma_isFlat_iff {α : Type u_1} {F : Set α} {ι : Type u_2} {M : ι → Matroid α} (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) : (Matroid.disjointSigma M hdj).IsFlat F ↔ (∀ (i : ι), (M i).IsFlat (F ∩ (M i).E)) ∧ F ⊆ ⋃ (i : ι), (M i).E

@[simp]

theorem Matroid.disjointSum_isFlat_iff {α : Type u_1} {F : Set α} {M N : Matroid α} (hdj : Disjoint M.E N.E) : (M.disjointSum N hdj).IsFlat F ↔ M.IsFlat (F ∩ M.E) ∧ N.IsFlat (F ∩ N.E) ∧ F ⊆ M.E ∪ N.E

@[simp]

theorem Matroid.sum_isFlat_iff {α : Type u_1} {M : Matroid α} {β : Type u_3} {N : Matroid β} (F : Set (α ⊕ β)) : (M.sum N).IsFlat F ↔ M.IsFlat (Sum.inl ⁻¹' F) ∧ N.IsFlat (Sum.inr ⁻¹' F)