closure_loops_union_eq — Mathlib

English

The closure of the union of loops with X equals the closure of X, since loops can be added freely to X without changing closure.

Русский

Замыкание объединения петель с X равно замыканию X, поскольку петли можно свободно добавлять к X без изменения замыкания.

LaTeX

$$$ M.closure( M.loops \cup X ) = M.closure X $$$

Lean4

@[simp]
theorem closure_loops_union_eq (M : Matroid α) (X : Set α) : M.closure (M.loops ∪ X) = M.closure X := by
  simp [union_comm]

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