fundCircuit_eq_of_mem — Mathlib

English

The member e is in the fundamental circuit: e ∈ fundCircuit e I.

Русский

Член e принадлежит фундаментальному циклу: e ∈ fundCircuit e I.

LaTeX

$$$e \in fundCircuit\ M\ e\ I$$$

Lean4

/-- The fundamental isCircuit of `e` and `X` has the junk value `{e}` if `e ∈ X` -/
theorem fundCircuit_eq_of_mem (heX : e ∈ X) : 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]
  exact fun b hbX h ↦ h _ (singleton_subset_iff.2 heX) Subset.rfl

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