closure_diff_eq_self — Mathlib

English

If Y is contained in the closure of X \\ Y, then closure(X \\ Y) equals closure(X).

Русский

Если Y ⊆ closure(X \\ Y), то closure(X \\ Y) = closure(X).

LaTeX

$$$ Y \\subseteq M.\\mathrm{closure}(X \\setminus Y) \\Rightarrow M.\\mathrm{closure}(X \\setminus Y) = M.\\mathrm{closure}(X) $$$

Lean4

theorem closure_diff_eq_self (h : Y ⊆ M.closure (X \ Y)) : M.closure (X \ Y) = M.closure X := by
  rw [← diff_union_inter X Y, ← closure_union_closure_left_eq,
    union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, diff_union_inter]

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