ord_mono

Mathlib.SetTheory.Ordinal.Basic

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

English

The map o ↦ ord(o) is monotone: if a ≤ b then ord(a) ≤ ord(b).

Русский

Отображение o ↦ ord(o) монотонно: если a ≤ b, то ord(a) ≤ ord(b).

LaTeX

$$$ \forall a,b\, (a\le b) \Rightarrow \operatorname{ord}(a) \le \operatorname{ord}(b) $$$

Lean4

@[mono]
theorem ord_mono : Monotone ord :=
  gc_ord_card.monotone_l

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

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

Разделы

Аффилиация

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