closure_insert_isColoop_eq — Mathlib

English

Let M be a matroid on α and e a coloops of M. For every subset X of α, the closure of X together with e equals the closure of X with e adjoined: cl_M(X ∪ {e}) = cl_M(X) ∪ {e}.

Русский

Пусть M — матроид на α, и e — колооп M. Для любого подмножества X ⊆ α выполняется: замыкание_M(X ∪ {e}) = замыкание_M(X) ∪ {e}.

LaTeX

$$$$ \operatorname{cl}_M(X \cup \{e\}) = \operatorname{cl}_M(X) \cup \{e\}. $$$$

Lean4

theorem closure_insert_isColoop_eq (X : Set α) (he : M.IsColoop e) : M.closure (insert e X) = insert e (M.closure X) :=
  by rw [← union_singleton, closure_union_eq_of_subset_coloops _ (by simpa), union_singleton]

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