nhdsSet_interior

Mathlib.Topology.NhdsSet

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

English

The set-neighborhoods filter of the interior of s equals the principal filter of the interior of s.

Русский

Фильтр множеств-окрестностей interior(s) равен принципальному фильтру interior(s).

LaTeX

$$$ 𝓝ˢ (\operatorname{interior} s) = 𝓟 (\operatorname{interior} s) $$$

Lean4

@[simp]
theorem nhdsSet_interior : 𝓝ˢ (interior s) = 𝓟 (interior s) :=
  isOpen_interior.nhdsSet_eq

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

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

Разделы

Аффилиация

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