closure_biUnion_closure_eq_closure_biUnion

English

For a family Xs and a set A, the closure of the union over i ∈ A of closures equals the closure of the union over i ∈ A of Xs(i) when all Xs(i) closures match.

Русский

Для семейства Xs и множества A выполнено: cl(⋃ i ∈ A cl(Xi)) = cl(⋃ i ∈ A Xi), если для всех i ∈ A cl(Xi) = cl(Xi).

LaTeX

$$$\\operatorname{cl}(\\bigcup_{i \\in A} \\operatorname{cl}(X_i)) = \\operatorname{cl}(\\bigcup_{i \\in A} X_i)$$$

Lean4

theorem closure_biUnion_closure_eq_closure_biUnion (M : Matroid α) (Xs : ι → Set α) (A : Set ι) :
    M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i) := by
  rw [biUnion_eq_iUnion, M.closure_iUnion_closure_eq_closure_iUnion, biUnion_eq_iUnion]

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