closure_union_congr_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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