nhdsKer_singleton

Mathlib.Topology.Order.UpperLowerSetTopology

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

English

The neighborhood kernel of a singleton {a} is the right-closed interval Iic a.

Русский

Окружное ядро множества {a} равно Iic a.

LaTeX

$$$$ \\mathrm{nhdsKer}({a}) = \\mathrm{Iic}(a). $$$$

Lean4

@[simp]
theorem nhdsKer_singleton (a : α) : nhdsKer { a } = Iic a := by
  rw [nhdsKer_eq_lowerClosure, lowerClosure_singleton, LowerSet.coe_Iic]

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

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

Разделы

Аффилиация

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