English
Let s and t be subsets of a topological space X. Then the frontier of s ∪ t is contained in the union of (frontier s ∩ closure tᶜ) and (closure sᶜ ∩ frontier t).
Русский
Пусть s и t — подмножества в топологическом пространстве X. Тогда граница s ∪ t принадлежит объединению (граница s ∩ closure tᶜ) и (closure sᶜ ∩ граница t).
LaTeX
$$$\\operatorname{frontier}(s \\cup t) \\subseteq (\\operatorname{frontier}(s) \\cap \\overline{t^{c}}) \\cup (\\overline{s^{c}} \\cap \\operatorname{frontier}(t))$$$
Lean4
theorem frontier_union_subset (s t : Set X) : frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t := by
simpa only [frontier_compl, ← compl_union] using frontier_inter_subset sᶜ tᶜ
