English
If closure s and closure t are disjoint, then interior(s ∪ t) = interior(s) ∪ interior(t).
Русский
Еслиclosure s и closure t не пересекаются, то int(s ∪ t) = int(s) ∪ int(t).
LaTeX
$$(\\operatorname{Disjoint}(\\overline{s}, \\overline{t})) \\\\Rightarrow \\\\operatorname{int}(s \\\\cup t) = \\\\operatorname{int}(s) \\\\cup \\\\operatorname{int}(t)$$
Lean4
theorem interior_union_of_disjoint_closure (h : Disjoint (closure s) (closure t)) :
interior (s ∪ t) = interior s ∪ interior t :=
by
have full : interior sᶜ ∪ interior tᶜ = univ := by simpa [disjoint_iff, ← compl_inter] using h
refine subset_antisymm ?_ subset_interior_union
rw [← (interior _).inter_univ, ← full, inter_union_distrib_left]
exact
union_subset (interior_union_inter_interior_compl_left_subset.trans subset_union_right)
(interior_union_inter_interior_compl_right_subset.trans subset_union_left)
