closure_iUnion_congr — Mathlib

English

If for every i, the closures of Xs(i) and Ys(i) are equal, then the closures of the unions are equal.

Русский

Если для каждого i выполнено cl(X_i) = cl(Y_i), то cl(⋃ X_i) = cl(⋃ Y_i).

LaTeX

$$$(\\forall i, \\operatorname{cl}(X_i) = \\operatorname{cl}(Y_i)) \\Rightarrow \\operatorname{cl}(\\bigcup_i X_i) = \\operatorname{cl}(\\bigcup_i Y_i)$$$

Lean4

theorem closure_iUnion_congr (Xs Ys : ι → Set α) (h : ∀ i, M.closure (Xs i) = M.closure (Ys i)) :
    M.closure (⋃ i, Xs i) = M.closure (⋃ i, Ys i) := by simp [h, ← M.closure_iUnion_closure_eq_closure_iUnion]

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