English
Let X be a topological space and s, t be subsets of X. Then the frontier of s ∩ t is contained in the union of (frontier s ∩ closure t) and (closure s ∩ frontier t).
Русский
Пусть X — топологическое пространство и s, t — подмножества X. Тогда граница s ∩ t принадлежит объединению (граница s ∩closure t) и (closure s ∩ граница t).
LaTeX
$$$\\operatorname{frontier}(s \\cap t) \\subseteq (\\operatorname{frontier}(s) \\cap \\overline{t}) \\cup (\\overline{s} \\cap \\operatorname{frontier}(t))$$$
Lean4
theorem frontier_inter_subset (s t : Set X) : frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t :=
by
simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]
refine (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq ?_
simp only [inter_union_distrib_left, inter_assoc, inter_comm (closure t)]
