English
Let X be a topological space and s,t ⊆ X. Then closure(s) \\ closure(t) ⊆ closure(s \\ t).
Русский
Пусть X — топологическое пространство, s,t ⊆ X. Тогда cl(s) \\ cl(t) ⊆ cl(s \\ t).
LaTeX
$$$\\\\overline{s} \\setminus \\\\overline{t} \\subseteq \\\\overline{\\\\left( s \\setminus t \\\\right)}$$$
Lean4
theorem closure_diff : closure s \ closure t ⊆ closure (s \ t) :=
calc
closure s \ closure t = (closure t)ᶜ ∩ closure s := by simp only [diff_eq, inter_comm]
_ ⊆ closure ((closure t)ᶜ ∩ s) := (isOpen_compl_iff.mpr <| isClosed_closure).inter_closure
_ = closure (s \ closure t) := by simp only [diff_eq, inter_comm]
_ ⊆ closure (s \ t) := closure_mono <| diff_subset_diff (Subset.refl s) subset_closure
