closure_union_closure_empty_eq — Mathlib

English

For a collection Xs of sets, the closure of the union of the closures over all sets in Xs equals the closure of the sUnion of Xs.

Русский

Для множества Xs наборов: cl(⋃ X ∈ Xs cl(X)) = cl(⋃₀ Xs).

LaTeX

$$$\\operatorname{cl}(\\bigcup X \\in Xs, \\operatorname{cl} X) = \\operatorname{cl}(\\bigcup_0 Xs)$$$

Lean4

@[simp]
theorem closure_union_closure_empty_eq (M : Matroid α) (X : Set α) : M.closure X ∪ M.closure ∅ = M.closure X :=
  union_eq_self_of_subset_right (M.closure_subset_closure (empty_subset _))

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