fundCircuit_eq_of_notMem_ground — Mathlib

English

If e is not in the ground set E of M, then for any subset X, the fundamental circuit of e with respect to X is the singleton {e}.

Русский

Если элемент e не принадлежит базовому множеству E матроида M, то для любой подмножества X фундаментальная окружность e относительно X равна {e}.

LaTeX

$$$\\forall \\alpha\\ (M : Matroid \\alpha)\\ (X : Set \\alpha)\\ (e : \\alpha), e \\notin M.E \\Rightarrow M.fundCircuit\\ e\\ X = \\{ e \\}$$$

Lean4

theorem fundCircuit_eq_of_notMem_ground (heX : e ∉ M.E) : M.fundCircuit e X = { e } :=
  by
  suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure { e } ⊆ M.closure t → a ∈ t) → a = e by
    simpa [subset_antisymm_iff, fundCircuit]
  simp_rw [← M.closure_inter_ground { e }, singleton_inter_eq_empty.2 heX]
  exact fun a haX h ↦ by simpa using h ∅ (empty_subset X) rfl.subset

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