enumOrd_strictMono

Mathlib.SetTheory.Ordinal.Enum

URI: https://scilib.ai/kg/mathlib#Ordinal.enumOrd_strictMono

English

If s is not bounded above, then enumOrd s is strictly monotone.

Русский

Если s не ограничено сверху, то enumOrd s является строго монотонной функцией.

LaTeX

$$$\forall s,\ \neg BddAbove\, s \Rightarrow \text{StrictMono}(\operatorname{enumOrd} s)$$$

Lean4

theorem enumOrd_strictMono (hs : ¬BddAbove s) : StrictMono (enumOrd s) := fun a b ↦ (enumOrd_mem_aux hs b).2 a

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

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

Разделы

Аффилиация

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