theorem Matroid.IsFlat.eRk_eq_zero_iff {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : M.eRk F = 0 ↔ F = M.loops

def Matroid.IsPoint {α : Type u_1} (M : Matroid α) (P : Set α) : Prop

Equations

• M.IsPoint P = (M.IsFlat P ∧ M.eRk P = 1)

theorem Matroid.IsPoint.isFlat {α : Type u_1} {M : Matroid α} {P : Set α} (hP : M.IsPoint P) : M.IsFlat P

theorem Matroid.IsPoint.eRk {α : Type u_1} {M : Matroid α} {P : Set α} (hP : M.IsPoint P) : M.eRk P = 1

theorem Matroid.IsPoint.subset_ground {α : Type u_1} {M : Matroid α} {P : Set α} (hP : M.IsPoint P) : P ⊆ M.E

theorem Matroid.IsPoint.isRkFinite {α : Type u_1} {M : Matroid α} {P : Set α} (hP : M.IsPoint P) : M.IsRkFinite P

theorem Matroid.IsNonloop.closure_isPoint {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) : M.IsPoint (M.closure {e})

theorem Matroid.loops_covBy_iff {α : Type u_1} {M : Matroid α} {P : Set α} : M.loops ⋖[M] P ↔ M.IsPoint P

theorem Matroid.IsPoint.covBy {α : Type u_1} {M : Matroid α} {P : Set α} (hP : M.IsPoint P) : M.loops ⋖[M] P

theorem Matroid.IsPoint.exists_eq_closure_isNonloop {α : Type u_1} {M : Matroid α} {P : Set α} (hP : M.IsPoint P) : ∃ (e : α), M.IsNonloop e ∧ P = M.closure {e}

theorem Matroid.IsPoint.eq_closure_of_mem {α : Type u_1} {M : Matroid α} {P : Set α} {e : α} (hP : M.IsPoint P) (he : M.IsNonloop e) (heP : e ∈ P) : P = M.closure {e}

theorem Matroid.isPoint_iff_exists_eq_closure_isNonloop {α : Type u_1} {M : Matroid α} {P : Set α} : M.IsPoint P ↔ ∃ (e : α), M.IsNonloop e ∧ P = M.closure {e}

theorem Matroid.IsPoint.isNonloop {α : Type u_1} {M : Matroid α} {e : α} (hP : M.IsPoint {e}) : M.IsNonloop e

theorem Matroid.IsPoint.insert_indep {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsPoint {e}) (f : α) (hf : f ∈ M.E := by aesop_mat) : M.Indep {e, f}

theorem Matroid.isPoint_singleton_iff {α : Type u_1} {M : Matroid α} {e : α} [M.Nonempty] : M.IsPoint {e} ↔ ∀ f ∈ M.E, M.Indep {e, f}

theorem Matroid.IsPoint.loopless_of_singleton {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsPoint {e}) : M.Loopless

theorem Matroid.isPoint_contract_iff {α : Type u_1} {M : Matroid α} {P C : Set α} (hC : C ⊆ M.E := by aesop_mat) : (M.contract C).IsPoint P ↔ (M.closure C ⋖[M] (C ∪ P)) ∧ Disjoint P C

def Matroid.isPointContractCovByEquiv {α : Type u_1} (M : Matroid α) (C : Set α) : { P : Set α // (M.contract C).IsPoint P } ≃ { F : Set α // M.closure C ⋖[M] F }

Points of M ／ C are equivalent to flats covering M.closure C.

Equations

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

@[simp]

theorem Matroid.isPointContractCovByEquiv_symm_apply_coe {α : Type u_1} (M : Matroid α) (C : Set α) (P : { F : Set α // M.closure C ⋖[M] F }) : ↑((M.isPointContractCovByEquiv C).symm P) = ↑P \ C

@[simp]

theorem Matroid.isPointContractCovByEquiv_apply_coe {α : Type u_1} (M : Matroid α) (C : Set α) (P : { P : Set α // (M.contract C).IsPoint P }) : ↑((M.isPointContractCovByEquiv C) P) = ↑P ∪ M.closure C

theorem Matroid.IsPoint.eq_or_eq_of_isFlat_of_subset {α : Type u_1} {M : Matroid α} {F P : Set α} (hP : M.IsPoint P) (hF : M.IsFlat F) (h : F ⊆ P) : F = M.loops ∨ F = P

theorem Matroid.IsPoint.subset_or_inter_eq_loops_of_isFlat {α : Type u_1} {M : Matroid α} {F P : Set α} (hP : M.IsPoint P) (hF : M.IsFlat F) : P ⊆ F ∨ P ∩ F = M.loops

@[reducible, inline]

abbrev Matroid.IsLine {α : Type u_1} (M : Matroid α) (L : Set α) : Prop

Equations

• M.IsLine L = (M.IsFlat L ∧ M.eRk L = 2)

theorem Matroid.IsLine.isFlat {α : Type u_1} {M : Matroid α} {L : Set α} (hL : M.IsLine L) : M.IsFlat L

theorem Matroid.IsLine.eRk {α : Type u_1} {M : Matroid α} {L : Set α} (hL : M.IsLine L) : M.eRk L = 2

theorem Matroid.IsLine.subset_ground {α : Type u_1} {M : Matroid α} {L : Set α} (hL : M.IsLine L) : L ⊆ M.E

theorem Matroid.IsLine.isRkFinite {α : Type u_1} {M : Matroid α} {L : Set α} (hL : M.IsLine L) : M.IsRkFinite L

theorem Matroid.IsLine.mem_iff_covBy {α : Type u_1} {M : Matroid α} {L : Set α} {e : α} (hL : M.IsLine L) (he : M.IsNonloop e) : e ∈ L ↔ M.closure {e} ⋖[M] L

theorem Matroid.IsNonloop.closure_covBy_iff {α : Type u_1} {M : Matroid α} {L : Set α} {e : α} (he : M.IsNonloop e) : M.closure {e} ⋖[M] L ↔ M.IsLine L ∧ e ∈ L

def Matroid.IsNonloop.LineContractElemPointEquiv {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) : { P : Set α // (M.contract {e}).IsPoint P } ≃ { L : Set α // M.IsLine L ∧ e ∈ L }

Equations

• he.LineContractElemPointEquiv = (M.isPointContractCovByEquiv {e}).trans (Equiv.subtypeEquivRight ⋯)

@[reducible, inline]

abbrev Matroid.IsPlane {α : Type u_1} (M : Matroid α) (P : Set α) : Prop

Equations

• M.IsPlane P = (M.IsFlat P ∧ M.eRk P = 3)

theorem Matroid.IsPlane.isFlat {α : Type u_1} {M : Matroid α} {P : Set α} (hP : M.IsPlane P) : M.IsFlat P

theorem Matroid.IsPlane.eRk {α : Type u_1} {M : Matroid α} {P : Set α} (hP : M.IsPlane P) : M.eRk P = 3