English
The complement of the frontier is the union of the interior of s and the interior of the complement of s: (frontier(s))^c = interior(s) ∪ interior(s^c).
Русский
Комплемент границы равен объединению interior(s) и interior(s^c): (frontier(s))^c = interior(s) ∪ interior(s^c).
LaTeX
$$$ (\\operatorname{frontier}(s))^c = \\operatorname{interior}(s) \\cup \\operatorname{interior}(s^c) $$$
Lean4
theorem compl_frontier_eq_union_interior : (frontier s)ᶜ = interior s ∪ interior sᶜ :=
by
rw [frontier_eq_inter_compl_interior]
simp only [compl_inter, compl_compl]