scottHausdorff_le_isLawson

Mathlib.Topology.Order.LawsonTopology

URI: https://scilib.ai/kg/mathlib#Topology.scottHausdorff_le_isLawson

English

Scott-Hausdorff topology on α is weaker than the Lawson topology L when assumptions hold.

Русский

Топология Scott-Hausdorff на α слабее топологии Lawson при соблюдении условий.

LaTeX

$$$\text{scottHausdorff }(\alpha)\ univ \le L$$$

Lean4

theorem scottHausdorff_le_isLawson : scottHausdorff α univ ≤ L :=
  by
  rw [@IsLawson.topology_eq_lawson α _ L _]
  exact scottHausdorff_le_lawson

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

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

Разделы

Аффилиация

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