def Matroid.FlatOf {α : Type u_1} (M : Matroid α) : Type u_1

Equations

• Matroid.FlatOf M = { F : Set α // M.IsFlat F }

@[instance_reducible]

instance Matroid.instCoeOutFlatOfSet {α : Type u_1} {M : Matroid α} : CoeOut (FlatOf M) (Set α)

Equations

• Matroid.instCoeOutFlatOfSet = { coe := fun (F : Matroid.FlatOf M) => ↑F }

@[simp]

theorem Matroid.FlatOf.coe_isFlat {α : Type u_1} {M : Matroid α} (F : FlatOf M) : M.IsFlat ↑F

def Matroid.IsFlat.toFlatOf {α : Type u_1} {M : Matroid α} {F : Set α} (h : M.IsFlat F) : FlatOf M

Equations

• h.toFlatOf = ⟨F, h⟩

def Matroid.flatClosure {α : Type u_1} (M : Matroid α) (X : Set α) : FlatOf M

Equations

• M.flatClosure X = ⟨M.closure X, ⋯⟩

@[simp]

theorem Matroid.coe_flatClosure {α : Type u_1} (M : Matroid α) (X : Set α) : ↑(M.flatClosure X) = M.closure X

@[simp]

theorem Matroid.FlatOf.coe_inj {α : Type u_1} {M : Matroid α} {F F' : FlatOf M} : ↑F = ↑F' ↔ F = F'

theorem Matroid.FlatOf.coe_subset_ground {α : Type u_1} {M : Matroid α} (F : FlatOf M) : ↑F ⊆ M.E

@[instance_reducible]

instance Matroid.flatPartialOrder {α : Type u_1} (M : Matroid α) : PartialOrder (FlatOf M)

Equations

• M.flatPartialOrder = { le := fun (F₁ F₂ : Matroid.FlatOf M) => ↑F₁ ⊆ ↑F₂, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[simp]

theorem Matroid.FlatOf.le_iff {α : Type u_1} {M : Matroid α} {F F' : FlatOf M} : F ≤ F' ↔ ↑F ⊆ ↑F'

@[simp]

theorem Matroid.FlatOf.lt_iff {α : Type u_1} {M : Matroid α} {F F' : FlatOf M} : F < F' ↔ ↑F ⊂ ↑F'

theorem Matroid.flatClosure_mono {α : Type u_1} (M : Matroid α) : Monotone M.flatClosure

@[instance_reducible]

instance Matroid.flatLattice {α : Type u_1} (M : Matroid α) : CompleteLattice (FlatOf M)

The flats of a matroid form a complete lattice.

Equations

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

@[simp]

theorem Matroid.FlatOf.coe_top {α : Type u_1} (M : Matroid α) : ↑⊤ = M.E

@[simp]

theorem Matroid.FlatOf.coe_bot {α : Type u_1} (M : Matroid α) : ↑⊥ = M.loops

@[simp]

theorem Matroid.FlatOf.coe_sup {α : Type u_1} {M : Matroid α} (F₁ F₂ : FlatOf M) : ↑(F₁ ⊔ F₂) = M.closure (↑F₁ ∪ ↑F₂)

@[simp]

theorem Matroid.FlatOf.coe_inf {α : Type u_1} {M : Matroid α} (F₁ F₂ : FlatOf M) : ↑(F₁ ⊓ F₂) = ↑F₁ ∩ ↑F₂

@[simp]

theorem Matroid.FlatOf.coe_sSup {α : Type u_1} {M : Matroid α} (Fs : Set (FlatOf M)) : ↑(sSup Fs) = M.closure (⋃ F ∈ Fs, ↑F)

@[simp]

theorem Matroid.FlatOf.coe_sInf {α : Type u_1} {M : Matroid α} (Fs : Set (FlatOf M)) : ↑(sInf Fs) = (⋂ F ∈ Fs, ↑F) ∩ M.E

theorem Matroid.FlatOf.coe_sInf' {α : Type u_1} {M : Matroid α} {Fs : Set (FlatOf M)} (hne : Fs.Nonempty) : ↑(sInf Fs) = ⋂ F ∈ Fs, ↑F

def Matroid.CovBy {α : Type u_1} (M : Matroid α) (F₀ F₁ : Set α) : Prop

F₀ ⋖[M] F₁ means that F₀ and F₁ are strictly nested flats with no flat between them. Defined in terms of CovBy in the lattice of flats.

Equations

• (F₀ ⋖[M] F₁) = ∃ (h₀ : M.IsFlat F₀) (h₁ : M.IsFlat F₁), h₀.toFlatOf ⋖ h₁.toFlatOf

def Matroid.WCovBy {α : Type u_1} (M : Matroid α) (F₀ F₁ : Set α) : Prop

Equations

• (F₀ ⩿[M] F₁) = ∃ (h₀ : M.IsFlat F₀) (h₁ : M.IsFlat F₁), h₀.toFlatOf ⩿ h₁.toFlatOf

def Matroid.«term_⋖[_]_» : Lean.TrailingParserDescr

Equations

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

def Matroid.«term_⩿[_]_» : Lean.TrailingParserDescr

Equations

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

theorem Matroid.FlatOf.covBy_iff {α : Type u_1} {M : Matroid α} (F₀ F₁ : FlatOf M) : F₀ ⋖ F₁ ↔ ↑F₀ ⋖[M] ↑F₁

theorem Matroid.FlatOf.wcovBy_iff {α : Type u_1} {M : Matroid α} (F₀ F₁ : FlatOf M) : F₀ ⩿ F₁ ↔ ↑F₀ ⩿[M] ↑F₁

theorem Matroid.covBy_iff {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} : F₀ ⋖[M] F₁ ↔ M.IsFlat F₀ ∧ M.IsFlat F₁ ∧ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.IsFlat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁

theorem Matroid.WCovBy.isFlat_left {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⩿[M] F₁) : M.IsFlat F₀

theorem Matroid.WCovBy.isFlat_right {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⩿[M] F₁) : M.IsFlat F₁

theorem Matroid.CovBy.isFlat_left {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : M.IsFlat F₀

theorem Matroid.CovBy.isFlat_right {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : M.IsFlat F₁

theorem Matroid.CovBy.subset_ground_left {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : F₀ ⊆ M.E

theorem Matroid.CovBy.subset_ground_right {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : F₁ ⊆ M.E

theorem Matroid.CovBy.ssubset {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : F₀ ⊂ F₁

theorem Matroid.CovBy.ne {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : F₀ ≠ F₁

theorem Matroid.CovBy.subset {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : F₀ ⊆ F₁

theorem Matroid.WCovBy.subset {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⩿[M] F₁) : F₀ ⊆ F₁

theorem Matroid.IsFlat.covBy_iff_wcovBy_and_ne {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) : F₀ ⋖[M] F₁ ↔ (F₀ ⩿[M] F₁) ∧ F₀ ≠ F₁

theorem Matroid.IsFlat.covBy_iff_wcovBy_and_ssubset {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) : F₀ ⋖[M] F₁ ↔ (F₀ ⩿[M] F₁) ∧ F₀ ⊂ F₁

@[simp]

theorem Matroid.IsFlat.wCovBy_self {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : F ⩿[M] F

theorem Matroid.IsFlat.wCovby_iff_covBy_or_eq {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) : F₀ ⩿[M] F₁ ↔ (F₀ ⋖[M] F₁) ∨ F₀ = F₁

theorem Matroid.WCovBy.covBy_of_ne {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⩿[M] F₁) (hne : F₀ ≠ F₁) : F₀ ⋖[M] F₁

theorem Matroid.WCovBy.eq_or_covBy {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⩿[M] F₁) : F₀ = F₁ ∨ (F₀ ⋖[M] F₁)

theorem Matroid.CovBy.wCovby {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : F₀ ⩿[M] F₁

theorem Matroid.IsFlat.covBy_iff_of_isFlat {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) : F₀ ⋖[M] F₁ ↔ F₀ ⊂ F₁ ∧ ∀ (F : Set α), M.IsFlat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁

theorem Matroid.IsFlat.wcovBy_iff_of_isFlat {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) : F₀ ⩿[M] F₁ ↔ F₀ ⊆ F₁ ∧ ∀ (F : Set α), M.IsFlat F → F₀ ⊆ F → F ⊆ F₁ → F = F₀ ∨ F = F₁

theorem Matroid.WCovBy.wCovBy_left_of_between {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (h : F₀ ⩿[M] F₁) (hF : M.IsFlat F) (hF₀F : F₀ ⊆ F) (hFF₁ : F ⊆ F₁) : F₀ ⩿[M] F

theorem Matroid.WCovBy.wCovBy_right_of_between {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (h : F₀ ⩿[M] F₁) (hF : M.IsFlat F) (hF₀F : F₀ ⊆ F) (hFF₁ : F ⊆ F₁) : F ⩿[M] F₁

theorem Matroid.CovBy.eq_or_eq {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) (hF : M.IsFlat F) (h₀ : F₀ ⊆ F) (h₁ : F ⊆ F₁) : F = F₀ ∨ F = F₁

theorem Matroid.CovBy.eq_of_subset_of_ssubset {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) (hF : M.IsFlat F) (hF₀ : F₀ ⊆ F) (hF₁ : F ⊂ F₁) : F = F₀

theorem Matroid.CovBy.eq_of_ssubset_of_subset {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) (hF : M.IsFlat F) (hF₀ : F₀ ⊂ F) (hF₁ : F ⊆ F₁) : F = F₁

theorem Matroid.CovBy.inter_eq_of_covby_of_ne {α : Type u_1} {M : Matroid α} {F₀ F₁ F₂ : Set α} (h₁ : F₀ ⋖[M] F₁) (h₂ : F₀ ⋖[M] F₂) (h_ne : F₁ ≠ F₂) : F₀ = F₁ ∩ F₂

theorem Matroid.CovBy.closure_insert_eq {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} {e : α} (h : F₀ ⋖[M] F₁) (he : e ∈ F₁ \ F₀) : M.closure (insert e F₀) = F₁

theorem Matroid.CovBy.exists_eq_closure_insert {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : ∃ e ∈ F₁ \ F₀, M.closure (insert e F₀) = F₁

theorem Matroid.CovBy.exists_eq_closure_insert' {α : Type u_1} {M : Matroid α} {F X : Set α} (h : M.closure X ⋖[M] F) : ∃ e ∈ F \ M.closure X, F = M.closure (insert e X)

theorem Matroid.IsFlat.covBy_iff_eq_closure_insert {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) : F₀ ⋖[M] F₁ ↔ ∃ e ∈ M.E \ F₀, F₁ = M.closure (insert e F₀)

theorem Matroid.CovBy.eRk_eq {α : Type u_1} {M : Matroid α} {F F' : Set α} (h : F ⋖[M] F') : M.eRk F' = M.eRk F + 1

theorem Matroid.Covby.eRk_eq_of_ssubset_of_subset {α : Type u_1} {M : Matroid α} {F X F' : Set α} (h : F ⋖[M] F') (hFX : F ⊂ X) (hXF' : X ⊆ F') : M.eRk X = M.eRk F + 1

theorem Matroid.CovBy.rk_eq_of_isRkFinite {α : Type u_1} {M : Matroid α} {F F' : Set α} (h : F ⋖[M] F') (hFin : M.IsRkFinite F) : M.rk F' = M.rk F + 1

theorem Matroid.closure_covBy_iff {α : Type u_1} {M : Matroid α} {F X : Set α} : M.closure X ⋖[M] F ↔ ∃ e ∈ M.E \ M.closure X, F = M.closure (insert e X)

theorem Matroid.closure_covBy_closure_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.closure X ⋖[M] M.closure Y ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.closure X ∧ M.closure (insert e X) = M.closure Y

theorem Matroid.IsFlat.covBy_closure_insert {α : Type u_1} {M : Matroid α} {F : Set α} {e : α} (hF : M.IsFlat F) (he : e ∉ F) (heE : e ∈ M.E := by aesop_mat) : F ⋖[M] M.closure (insert e F)

theorem Matroid.IsFlat.wCovBy_closure_insert {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) (e : α) : F ⩿[M] M.closure (insert e F)

theorem Matroid.IsFlat.wCovby_of_subset_closure_insert {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} {e : α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) (hss : F₀ ⊆ F₁) (hF₁e : F₁ ⊆ M.closure (insert e F₀)) : F₀ ⩿[M] F₁

theorem Matroid.Indep.closure_diff_covBy {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (he : e ∈ I) : M.closure (I \ {e}) ⋖[M] M.closure I

theorem Matroid.Indep.covBy_closure_insert {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (he : e ∈ M.E \ M.closure I) : M.closure I ⋖[M] M.closure (insert e I)

theorem Matroid.CovBy.eq_closure_insert_of_mem_diff {α : Type u_1} {M : Matroid α} {F F' : Set α} {e : α} (h : F ⋖[M] F') (he : e ∈ F' \ F) : F' = M.closure (insert e F)

theorem Matroid.IsFlat.covBy_iff_eRelRk_eq_one {α : Type u_1} {M : Matroid α} {F F₀ : Set α} (hF₀ : M.IsFlat F₀) (hF : M.IsFlat F) : F₀ ⋖[M] F ↔ F₀ ⊆ F ∧ M.eRelRk F₀ F = 1

theorem Matroid.IsFlat.covBy_iff_eRelRk_eq_one_of_subset {α : Type u_1} {M : Matroid α} {F F₀ : Set α} (hF₀ : M.IsFlat F₀) (hF : M.IsFlat F) (hss : F₀ ⊆ F) : F₀ ⋖[M] F ↔ M.eRelRk F₀ F = 1

theorem Matroid.IsFlat.covBy_iff_rk_eq_add_one {α : Type u_1} {M : Matroid α} {F F₀ : Set α} [M.RankFinite] (hF₀ : M.IsFlat F₀) (hF : M.IsFlat F) : F₀ ⋖[M] F ↔ F₀ ⊆ F ∧ M.rk F = M.rk F₀ + 1

theorem Matroid.CovBy.eRelRk_eq_one {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h : F₀ ⋖[M] F₁) : M.eRelRk F₀ F₁ = 1

theorem Matroid.CovBy.eRelRk_eq_eRelRk {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (h : F₀ ⋖[M] F) (h' : F₁ ⋖[M] F) : M.eRelRk F₀ F = M.eRelRk F₁ F

theorem Matroid.CovBy.eRk_eq_eRk {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (h : F₀ ⋖[M] F) (h' : F₁ ⋖[M] F) : M.eRk F₀ = M.eRk F₁

theorem Matroid.covBy_iff_eRelRk_eq_one {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} : F₀ ⋖[M] F₁ ↔ M.IsFlat F₀ ∧ M.IsFlat F₁ ∧ F₀ ⊆ F₁ ∧ M.eRelRk F₀ F₁ = 1

theorem Matroid.IsFlat.exists_unique_isFlat_of_notMem {α : Type u_1} {M : Matroid α} {F₀ : Set α} {e : α} (hF₀ : M.IsFlat F₀) (he : e ∈ M.E \ F₀) : ∃! F₁ : Set α, e ∈ F₁ ∧ (F₀ ⋖[M] F₁)

theorem Matroid.CovBy.eq_closure_union_of_covBy_of_ne {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (h₀ : F₀ ⋖[M] F) (h₁ : F₁ ⋖[M] F) (hne : F₀ ≠ F₁) : F = M.closure (F₀ ∪ F₁)

If F covers distinct flats F₀ and F₁, then F is their join.

theorem Matroid.IsFlat.exists_left_covBy_of_ssubset {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) (hss : F₀ ⊂ F₁) : ∃ (F : Set α), (F₀ ⋖[M] F) ∧ F ⊆ F₁

theorem Matroid.IsFlat.exists_covby_of_ne_ground {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) (hne : F ≠ M.E) : ∃ (F' : Set α), F ⋖[M] F'

theorem Matroid.IsFlat.exists_covBy_right_of_ssubset {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) (hss : F₀ ⊂ F₁) : ∃ (F : Set α), F₀ ⊆ F ∧ (F ⋖[M] F₁)

theorem Matroid.CovBy.covBy_closure_union_of_inter_covBy {α : Type u_1} {M : Matroid α} {F₀ F₁ : Set α} (h₀ : F₀ ∩ F₁ ⋖[M] F₀) (h₁ : F₀ ∩ F₁ ⋖[M] F₁) : F₀ ⋖[M] M.closure (F₀ ∪ F₁)

instance Matroid.instIsWeakUpperModularLatticeFlatOf {α : Type u_1} {M : Matroid α} : IsWeakUpperModularLattice (FlatOf M)

theorem Matroid.IsFlat.covBy_and_covBy_of_ssubset_of_ssubset_of_eRelRk_eq_two {α : Type u_1} {M : Matroid α} {F F₀ F₁ : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) (h : M.eRelRk F₀ F₁ = 2) (hF : M.IsFlat F) (h₀ : F₀ ⊂ F) (h₁ : F ⊂ F₁) : (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)

If M.eRelRk F₀ F₁ = 2 for flats F₀, F₁, then every flat strictly between F₀ and F₁ covers F₀ and is covered by F₁.

theorem Matroid.CovBy.covBy_and_covBy_of_covBy_of_ssubset_of_ssubset {α : Type u_1} {M : Matroid α} {F F' F₀ F₁ : Set α} (hF₀F' : F₀ ⋖[M] F') (hF'F₁ : F' ⋖[M] F₁) (hF : M.IsFlat F) (h₀ : F₀ ⊂ F) (h₁ : F ⊂ F₁) : (F₀ ⋖[M] F) ∧ (F ⋖[M] F₁)

If some flat is covered by F₁ and covers F₀, then this holds for every flat strictly between F₀ and F₁.

theorem Matroid.CovBy.insert_isBasis {α : Type u_1} {M : Matroid α} {I F F' : Set α} {e : α} (hFF' : F ⋖[M] F') (hI : M.IsBasis I F) (he : e ∈ F' \ F) : M.IsBasis (insert e I) F'

def Matroid.IsFlat.covByPartition {α : Type u_1} {M : Matroid α} {F : Set α} : M.IsFlat F → Partition (Set α)

The flats covering a flat F induce a partition of M.E \ F.

Equations

• x✝.covByPartition = Partition.ofPairwiseDisjoint' ⋯ ⋯

@[simp]

theorem Matroid.IsFlat.covByPartition_parts {α : Type u_1} {M : Matroid α} {F : Set α} (x✝ : M.IsFlat F) : x✝.covByPartition.parts = (fun (x : Set α) => x \ F) '' {F' : Set α | F ⋖[M] F'}

@[simp]

theorem Matroid.IsFlat.covByPartition_supp {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : hF.covByPartition.supp = M.E \ F

@[simp]

theorem Matroid.IsFlat.mem_covByPartition_iff {α : Type u_1} {M : Matroid α} {F X : Set α} (hF : M.IsFlat F) : X ∈ hF.covByPartition ↔ ∃ (F' : Set α), (F ⋖[M] F') ∧ F' \ F = X

@[simp]

theorem Matroid.IsFlat.partOf_covByPartition_eq {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) (e : α) : hF.covByPartition.partOf e = M.closure (insert e F) \ F

@[simp]

theorem Matroid.IsFlat.rel_covByPartition_iff {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) {e f : α} : hF.covByPartition e f ↔ e ∈ M.E \ F ∧ f ∈ M.E \ F ∧ M.closure (insert e F) = M.closure (insert f F)

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

def Matroid.IsFlat.equivCovByPartition {α : Type u_1} {M : Matroid α} {F₀ : Set α} (hF₀ : M.IsFlat F₀) : ↑↑hF₀.covByPartition ≃ { F : Set α // F₀ ⋖[M] F }

Cells of the covByPartition induced by F₀ are equivalent to flats covering F₀.

Equations

• hF₀.equivCovByPartition = { toFun := fun (F : ↑↑hF₀.covByPartition) => ⟨↑F ∪ F₀, ⋯⟩, invFun := fun (F : { F : Set α // F₀ ⋖[M] F }) => ⟨↑F \ F₀, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matroid.IsFlat.equivCovByPartition_apply_coe {α : Type u_1} {M : Matroid α} {F₀ : Set α} (hF₀ : M.IsFlat F₀) (F : ↑↑hF₀.covByPartition) : ↑(hF₀.equivCovByPartition F) = ↑F ∪ F₀

@[simp]

theorem Matroid.IsFlat.equivCovByPartition_symm_apply_coe {α : Type u_1} {M : Matroid α} {F₀ : Set α} (hF₀ : M.IsFlat F₀) (F : { F : Set α // F₀ ⋖[M] F }) : ↑(hF₀.equivCovByPartition.symm F) = ↑F \ F₀

theorem Matroid.IsFlat.inter_iUnion_closure_of_directed {α : Type u_1} {M : Matroid α} {F : Set α} [M.Finitary] {ι : Type u_2} {Xs : ι → Set α} (hF : M.IsFlat F) (hXs : ∀ (i : ι), M.IsFlat (Xs i)) (h_dir : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) Xs) : F ∩ M.closure (⋃ (i : ι), Xs i) = M.closure (⋃ (i : ι), F ∩ Xs i)

This lemma is stating that the lattice of flats of a finitary matroid is meet-continuous. This needs Finitary, even if the directed set is known to be a chain. A counterexample would be the matroid on [0,1] whose ground set is a circuit, where the Xs are the sets [0,x) for x < 1, and F = {1}.

theorem Matroid.finite_of_isChain_of_forall_isFlat {α : Type u_1} {M : Matroid α} [M.RankFinite] {Fs : Set (Set α)} (hFs : ∀ F ∈ Fs, M.IsFlat F) (hchain : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) Fs) : Fs.Finite

Every chain of flats in a finite-rank matroid is finite.