div_lt_div_right — Mathlib

English

Division by a fixed nonzero, noninfinite divisor preserves strict inequality when the numerators are compared.

Русский

Деление на фиксированный ненулевой, не бесконечный делитель сохраняет строгое неравенство при сравнении числителей.

LaTeX

$$\\forall a,b,c ∈ ENNReal, a < b ∧ c ≠ 0 ∧ c ≠ ∞ \\Rightarrow \\frac{a}{c} < \\frac{b}{c}$$

Lean4

@[gcongr]
protected theorem div_lt_div_right (hc₀ : c ≠ 0) (hc : c ≠ ∞) (hab : a < b) : a / c < b / c :=
  (ENNReal.div_lt_div_iff_left hc₀ hc).2 hab

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