nhdsKer_singleton

Mathlib.Topology.Order.UpperLowerSetTopology

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

English

The neighborhood kernel of a singleton {a} is the principal ray starting at a: Ici a.

Русский

Ядро окрестности множество-одиночки {a} равно Ici a = {x : a ≤ x}.

LaTeX

$$$ nhdsKer\{a\} = \mathrm{Ici}\,a.$$$

Lean4

@[simp]
theorem nhdsKer_singleton (a : α) : nhdsKer { a } = Ici a := by
  rw [nhdsKer_eq_upperClosure, upperClosure_singleton, UpperSet.coe_Ici]

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

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

Разделы

Аффилиация

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