instIsScottUnivSet

Mathlib.Topology.Order.ScottTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithScott.instIsScottUnivSet

English

For any α, the universal set in WithScott α is Scott (i.e., IsScott on univ).

Русский

Для любого α множество-единица в WithScott α является Scott.

LaTeX

$$$\text{IsScott}(WithScott(\alpha))\, univ$$$

Lean4

instance : IsScott (WithScott α) univ :=
  ⟨rfl⟩

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

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

Разделы

Аффилиация

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