top

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#CompleteLattice.ωScottContinuous.top

English

The top function ⊤ is ωScottContinuous.

Русский

Функция верхнего предела ⊤ непрерывна по ωScott.

LaTeX

$$$\omegaScottContinuous (\top : \alpha \to \beta)$$$

Lean4

theorem top : ωScottContinuous (⊤ : α → β) :=
  ωScottContinuous.of_monotone_map_ωSup ⟨monotone_const, fun c ↦ eq_of_forall_ge_iff fun a ↦ by simp⟩

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

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

Разделы

Аффилиация

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