interior_interior

Mathlib.Topology.Closure

URI: https://scilib.ai/kg/mathlib#interior_interior

English

Taking interior twice yields the same interior: int(int(s)) = int(s).

Русский

Повторное взятие interior дает тот же interior: int(int(s)) = int(s).

LaTeX

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

Lean4

@[simp]
theorem interior_interior : interior (interior s) = interior s :=
  isOpen_interior.interior_eq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru