le_mul_self — Mathlib

English

In a canonically ordered multiplicative structure, for all a,b,c, a ≤ b implies a·x ≤ b·x for any x, i.e., left multiplication is order-preserving.

Русский

В канонически упорядоченной умножимой структуре при любых a ≤ b выполняется a·x ≤ b·x для любого x; то есть левое умножение сохраняет порядок.

LaTeX

$$$\forall x,y,z\in \alpha\ (x \le y \Rightarrow z\cdot x \le z\cdot y)$$$

Lean4

@[to_additive]
theorem le_mul_self : a ≤ b * a :=
  CanonicallyOrderedMul.le_mul_self _ _

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