monotone

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.ContinuousHom.monotone

English

Every ωScottContinuous map is monotone.

Русский

Каждое ωScott непрерывное отображение монотонно.

LaTeX

$$$\text{monotone}(f)$ for $f : \alpha \to𝒄 \beta$$$

Lean4

protected theorem monotone (f : α →𝒄 β) : Monotone f :=
  f.monotone'

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

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

Разделы

Аффилиация

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