isLawson_le_isScott

Mathlib.Topology.Order.LawsonTopology

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

English

Given L is Lawson and S is Scott under appropriate hypotheses, L ≤ S.

Русский

При данных условиях, если L — Lawson, а S — Scott, то L ≤ S.

LaTeX

$$$\forall L S, [IsLawson α] [IsScott α\ univ] \Rightarrow L \le S$$$

Lean4

theorem isLawson_le_isScott : L ≤ S :=
  by
  rw [@IsScott.topology_eq α univ _ S _, @IsLawson.topology_eq_lawson α _ L _]
  exact inf_le_right

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

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

Разделы

Аффилиация

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