mul_div_mul_left_le — Mathlib

English

If 0 ≤ a/b, then c*a/(c*b) ≤ a/b for any c ≠ 0.

Русский

Если a/b неотрицательно, то c*a/(c*b) ≤ a/b для любого c ≠ 0.

LaTeX

$$$\forall a,b,c\in G_0,\ 0 \le a/b \land c \neq 0\Rightarrow c*a/(c*b) \le a/b$$$

Lean4

/-- Equality holds when `c ≠ 0`. See `mul_div_mul_left`. -/
theorem mul_div_mul_left_le (h : 0 ≤ a / b) : c * a / (c * b) ≤ a / b :=
  by
  obtain rfl | hc := eq_or_ne c 0
  · simpa
  · rw [mul_div_mul_left _ _ hc]

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