interior

Mathlib.Topology.Defs.Basic

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

English

The interior of a set s is the union of all open subsets of s.

Русский

interior множества s есть объединение всех открытых подмножетсв, входящих в s.

LaTeX

$$$\operatorname{interior}(s) = \bigcup_{t\text{ open},\ t\subseteq s} t$$$

Lean4

/-- The interior of a set `s` is the largest open subset of `s`. -/
def interior (s : Set X) : Set X :=
  ⋃₀ {t | IsOpen t ∧ t ⊆ s}

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

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

Разделы

Аффилиация

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