instPosMulStrictMono

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

For a > 0, the map x ↦ a · x is strictly increasing on ordinals.

Русский

Для a > 0 отображение x ↦ a · x строго возрастает на ординалах.

LaTeX

$$$\forall a,b\in \mathrm{Ordinal},\ a > 0 \Rightarrow \mathrm{strictMono}(\lambda x. a \cdot x)$$

Lean4

instance : PosMulStrictMono Ordinal where elim a _b _c h := (isNormal_mul_right a.2).strictMono h

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

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

Разделы

Аффилиация

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