English
Closure of interior of closure of interior s equals closure of interior s.
Русский
Замыкание внутренности замыкания внутренности множества равно замыканию внутренности множества.
LaTeX
$$$\overline{\operatorname{int}(\overline{\operatorname{int}(s)})} = \overline{\operatorname{int}(s)}$$$
Lean4
@[simp]
theorem closure_interior_idem : closure (interior (closure (interior s))) = closure (interior s) :=
isClosed_closure.closure_interior_subset.antisymm (closure_mono isOpen_interior.subset_interior_closure)