ωScottContinuous

Mathlib.Order.OmegaCompletePartialOrder

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

English

Logical equivalences relating IsLUB to omega-suprema via simple rewrites.

Русский

Логические эквивалентности между IsLUB и ωSup через простые преобразования.

LaTeX

$$$$ \forall {\alpha}, {p}, {q},\; Eq(\forall (b: \Exists p x), q b) (\forall x, p x \to q(\Exists x p x)). $$$$

Lean4

theorem _root_.ScottContinuous.ωScottContinuous (hf : ScottContinuous f) : ωScottContinuous f :=
  hf.scottContinuousOn

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

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

Разделы

Аффилиация

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