principal_le_nhdsSet

Mathlib.Topology.NhdsSet

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

English

The principal filter on a set s is below the set-neighborhoods filter of s: 𝓟 s ≤ 𝓝ˢ s.

Русский

Принципальный фильтр по множеству s лежит в фильтре множеств-окрестностей s: 𝓟 s ≤ 𝓝ˢ s.

LaTeX

$$$ 𝓟 s \le 𝓝ˢ s $$$

Lean4

theorem principal_le_nhdsSet : 𝓟 s ≤ 𝓝ˢ s := fun _s hs => (subset_interior_iff_mem_nhdsSet.mpr hs).trans interior_subset

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

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

Разделы

Аффилиация

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