interior_univ

Mathlib.Topology.Closure

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

English

The interior of the universal set is the universal set.

Русский

Интерьер множества единицы равен единице.

LaTeX

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

Lean4

@[simp]
theorem interior_univ : interior (univ : Set X) = univ :=
  isOpen_univ.interior_eq

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

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

Разделы

Аффилиация

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