le_mul_of_one_le_left' — Mathlib

English

If 1 ≤ b and right-monotone, then a ≤ a·b implies b ≥ 1; equivalently, a ≤ b·a given certain left-reflection.

Русский

Если 1 ≤ b и правое монотонное умножение, то a ≤ a·b эквивалентно b ≥ 1; или, в некоторых случаях, a ≤ b·a.

LaTeX

$$$\\forall a,b:\; a ≤ a\cdot b \Rightarrow 1 \le b$$$

Lean4

@[to_additive le_add_of_nonneg_left]
theorem le_mul_of_one_le_left' [MulRightMono α] {a b : α} (h : 1 ≤ b) : a ≤ b * a :=
  calc
    a = 1 * a := (one_mul a).symm
    _ ≤ b * a := mul_le_mul_right' h a

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