map_ωSup

Mathlib.Order.OmegaCompletePartialOrder

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

English

For any ωScott-continuous f, f(ωSup c) = ωSup (c.map f).

Русский

Для любого ωScott‑непрерывного f выполняется f(ωSup c) = ωSup (c.map f).

LaTeX

$$$$ f(\omegaSup c) = \omegaSup \bigl(c.map \langle f, f\text{.monotone} \rangle\bigr). $$$$

Lean4

theorem map_ωSup (hf : ωScottContinuous f) (c : Chain α) : f (ωSup c) = ωSup (c.map ⟨f, hf.monotone⟩) :=
  ωSup_eq_of_isLUB hf.isLUB

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

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

Разделы

Аффилиация

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