mul_inv_left_le — Mathlib

English

If b ≥ 0, then for any a, b ≤ a·(a⁻¹·b), and if a ≠ 0, equality holds: a·a⁻¹·b = b.

Русский

Если b ≥ 0, то для любого a имеет место неравенство b ≤ a·(a⁻¹·b); при этом равенство достигается, если a ≠ 0: a·a⁻¹·b = b.

LaTeX

$$$\forall a\,b\; (0 \le b) \Rightarrow b \le a \cdot (a^{-1} \cdot b) \\ \text{and } (a \neq 0 \Rightarrow a \cdot a^{-1} \cdot b = b)$$$

Lean4

/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel_left`. -/
theorem mul_inv_left_le (hb : 0 ≤ b) : a * (a⁻¹ * b) ≤ b := by obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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