closure_biUnion_closure_eq_closure_sUnion

English

For any collection Xs of subsets, the closure of the union of the closures over all X 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

theorem closure_biUnion_closure_eq_closure_sUnion (M : Matroid α) (Xs : Set (Set α)) :
    M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs) := by
  rw [sUnion_eq_iUnion, biUnion_eq_iUnion, closure_iUnion_closure_eq_closure_iUnion]

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