closure_interior_idem — Mathlib

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)

Похожие утверждения