nhds_eq_principal_Ici

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsUpperSet.nhds_eq_principal_Ici

English

The neighborhood at a equals the principal filter of Ici a.

Русский

Окрестность точки a равна принципиальному фильтру Ici a.

LaTeX

$$$ \mathcal{N}(a) = \mathcal{P}(\mathrm{Ici}\,a).$$$

Lean4

theorem nhds_eq_principal_Ici (a : α) : 𝓝 a = 𝓟 (Ici a) := by rw [← principal_nhdsKer_singleton, nhdsKer_singleton]

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

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

Разделы

Аффилиация

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