interior_eq_univ

Mathlib.Topology.Closure

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

← MathLib Explorer

English

The interior of a set equals the universal set if and only if the set equals the universal set.

Русский

interior(s) = univ ⇔ s = univ.

LaTeX

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

Lean4

@[simp]
theorem interior_eq_univ : interior s = univ ↔ s = univ :=
  ⟨fun h => univ_subset_iff.mp <| h.symm.trans_le interior_subset, fun h => h.symm ▸ interior_univ⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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