nhds_eq_principal_Iic

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsLowerSet.nhds_eq_principal_Iic

English

The neighborhood of a is the principal filter on the down-closed interval Iic a.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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