isLoop_tfae — Mathlib

English

For a Matroid M on α and an element e, the following five conditions are equivalent: e is a loop in M; e belongs to the closure of the empty set; {e} is a circuit; {e} is dependent; and for every base B of M, e belongs to E \ B (i.e., e is not contained in any base).

Русский

Для матроида M на множестве α и элемента e равны следующие пять условий: e — петля в M; e принадлежит замыканию пустого множества; {e} являетсяCircuit; {e} является зависимым множеством; и для каждого базиса B матроида M, e принадлежит E \ B (то есть e не принадлежит ни одному базису).

LaTeX

$$$ M.IsLoop\,e \iff e \in M.closure(\emptyset) \iff M.IsCircuit\{e\} \iff M.Dep\{e\} \iff \forall B\, (M.IsBase B \to e \in M.E \setminus B) $$$

Lean4

theorem isLoop_tfae (M : Matroid α) (e : α) :
    List.TFAE [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit { e }, M.Dep { e }, ∀ ⦃B⦄, M.IsBase B → e ∈ M.E \ B] :=
  by
  tfae_have 1 ↔ 2 := Iff.rfl
  tfae_have 2 ↔ 3 := by
    simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e), isCircuit_def, minimal_iff_forall_ssubset,
      ssubset_singleton_iff]
  tfae_have 2 ↔ 4 := by simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e)]
  tfae_have 4 ↔ 5 := by
    simp only [dep_iff, singleton_subset_iff, mem_diff, forall_and]
    refine
      ⟨fun h ↦ ⟨fun _ _ ↦ h.2, fun B hB heB ↦ h.1 (hB.indep.subset (by simpa))⟩, fun h ↦
        ⟨fun hi ↦ ?_, h.1 _ M.exists_isBase.choose_spec⟩⟩
    obtain ⟨B, hB, heB⟩ := hi.exists_isBase_superset
    exact h.2 _ hB (by simpa using heB)
  tfae_finish

Похожие утверждения