le_mul_left

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

If 0 < b, then for all ordinals a, a ≤ a · b.

Русский

Если 0 < b, тогда для любых порядковых чисел a выполняется a ≤ a · b.

LaTeX

$$$\forall a,b \in \mathrm{Ordinal},\ 0 < b \rightarrow a \le a \cdot b$$$

Lean4

theorem le_mul_left (a : Ordinal) {b : Ordinal} (hb : 0 < b) : a ≤ a * b :=
  by
  convert mul_le_mul_left' (one_le_iff_pos.2 hb) a
  rw [mul_one a]

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

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

Разделы

Аффилиация

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