English
If s is closed, then the interior of the frontier of s is empty: interior(frontier(s)) = ∅.
Русский
Если s замкнутое, то interior( frontier(s) ) = ∅.
LaTeX
$$$\\operatorname{Interior}(\\operatorname{frontier}(s)) = \\emptyset$$$
Lean4
/-- The frontier of a closed set has no interior point. -/
theorem interior_frontier (h : IsClosed s) : interior (frontier s) = ∅ :=
by
have A : frontier s = s \ interior s := h.frontier_eq
have B : interior (frontier s) ⊆ interior s := by rw [A]; exact interior_mono diff_subset
have C : interior (frontier s) ⊆ frontier s := interior_subset
have : interior (frontier s) ⊆ interior s ∩ (s \ interior s) := subset_inter B (by simpa [A] using C)
rwa [inter_diff_self, subset_empty_iff] at this
