le_mul_right — Mathlib

English

For 0 < b, we have a ≤ b · a for all ordinals a. (Multiplication on the left by a fixed right factor preserves order in the left argument.)

Русский

При 0 < b выполняется a ≤ b · a для всех ordinals a. (Умножение слева фиксированного правого множителя сохраняет порядок по левому аргументу.)

LaTeX

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

Lean4

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

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