nhdsKer_eq_lowerClosure

Mathlib.Topology.Order.UpperLowerSetTopology

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

English

nhdsKer s equals the lowerClosure of s, viewed as a subset.

Русский

nhdsKer s равно нижнему замыканию s как подмножество.

LaTeX

$$$$ \\mathrm{nhdsKer}(s) = \\uparrow(\\mathrm{lowerClosure}(s)). $$$$

Lean4

theorem nhdsKer_eq_lowerClosure (s : Set α) : nhdsKer s = ↑(lowerClosure s) := by ext;
  simp [mem_nhdsKer_iff_specializes, specializes_iff_le]

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

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

Разделы

Аффилиация

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