mem_closure_iff_exists_isCircuit — Mathlib

English

For e ∉ X, e is in the closure of X iff there exists a circuit C ⊆ insert e X with e ∈ C.

Русский

Для e, не принадлежащего X, e ∈ closure(X) тогда и только тогда, когда существует окружность C ⊆ insert e X такая, что e ∈ C.

LaTeX

$$$\\forall {\\alpha} {M : Matroid \\alpha} {X : Set α} {e : α}, e \\notin X \\Rightarrow (e \\in M.closure X \\iff \\exists C \\subseteq insert e X, M.IsCircuit C \\land e \\in C)$$$

Lean4

theorem mem_closure_iff_exists_isCircuit (he : e ∉ X) : e ∈ M.closure X ↔ ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C :=
  ⟨fun h ↦ exists_isCircuit_of_mem_closure h he, fun ⟨C, hCX, hC, heC⟩ ↦
    mem_of_mem_of_subset (hC.mem_closure_diff_singleton_of_mem heC) (M.closure_subset_closure (by simpa))⟩

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