closure_union_congr_right — Mathlib

English

If closure of Y equals closure of Y', then closure of X ∪ Y equals closure of X ∪ Y'.

Русский

Если cl(Y) = cl(Y'), то cl(X ∪ Y) = cl(X ∪ Y').

LaTeX

$$$\\operatorname{cl}(Y) = \\operatorname{cl}(Y') \\Rightarrow \\operatorname{cl}(X \\cup Y) = \\operatorname{cl}(X \\cup Y')$$$

Lean4

theorem closure_union_congr_right {Y' : Set α} (h : M.closure Y = M.closure Y') :
    M.closure (X ∪ Y) = M.closure (X ∪ Y') := by
  rw [← M.closure_union_closure_right_eq, h, M.closure_union_closure_right_eq]

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