isOpen_univ

Mathlib.Topology.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#Scott.isOpen_univ

English

The entire space is open in the Scott topology.

Русский

В Scott-топологии всякое пространство открыто.

LaTeX

$$$IsOpen(\text{univ}).$$$

Lean4

theorem isOpen_univ : IsOpen α univ :=
  @CompleteLattice.ωScottContinuous.top α Prop _ _

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

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

Разделы

Аффилиация

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