ord_strictMono

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.ord_strictMono

English

The map o ↦ ord(o) is strictly increasing: if a < b then ord(a) < ord(b).

Русский

Отображение o ↦ ord(o) строго возрастает: если a < b, то ord(a) < ord(b).

LaTeX

$$$ \forall a,b\, (a

Lean4

@[mono]
theorem ord_strictMono : StrictMono ord :=
  gciOrdCard.strictMono_l

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

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

Разделы

Аффилиация

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