const

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.ωScottContinuous.const

English

If a Chain of Part α has no element, its ωSup is none.

Русский

Если цепь Part α не содержит элементов, то ωSup равен none.

LaTeX

$$$$ \text{If } \neg \exists a, \text{some } a \in c, \text{ then } Part.\omegaSup c = none. $$$$

Lean4

theorem const {x : β} : ωScottContinuous (Function.const α x) := by
  simp [ωScottContinuous, ScottContinuousOn, Set.range_nonempty]

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

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

Разделы

Аффилиация

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