interior_closure_idem — Mathlib

English

Interior of closure of interior s equals interior s.

Русский

Внутреннее closure внутренности множества равно внутренности множества.

LaTeX

$$$\operatorname{int}(\overline{\operatorname{int}(s)}) = \operatorname{int}(s)$$$

Lean4

@[simp]
theorem interior_closure_idem : interior (closure (interior (closure s))) = interior (closure s) :=
  (interior_mono isClosed_closure.closure_interior_subset).antisymm isOpen_interior.subset_interior_closure

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