nhds_top

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#nhds_top

English

In the trivial topology, the neighborhood filter at any point is the top filter: nhds_{⊤}(a) = ⊤ for all a.

Русский

В тривиальной топологии окрестности любой точки образуют верхний фильтр: nhds_{⊤}(a) = ⊤ для всех a.

LaTeX

$$$$ \mathrm{nhds}_{\top}(a) = \top. $$$$

Lean4

theorem nhds_top {a : α} : @nhds α ⊤ a = ⊤ :=
  (gc_nhds a).u_top

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

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

Разделы

Аффилиация

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