instIsLawson

Mathlib.Topology.Order.LawsonTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithLawson.instIsLawson

English

WithLawson α is a Lawson space whenever α is a preorder.

Русский

WithLawson α является Lawson-пространством, когда α — упорядоченное множество.

LaTeX

$$$\forall {\alpha},\ [\operatorname{Preorder} \alpha] \Rightarrow \operatorname{IsLawson}(\mathrm{WithLawson}\;\alpha)$$$

Lean4

instance instIsLawson : IsLawson (WithLawson α) :=
  ⟨rfl⟩

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

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

Разделы

Аффилиация

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