lt_div_iff_mul_lt — Mathlib

English

For ENNReal, c < a / b ⇔ c b < a, under suitable nondegeneracy conditions.

Русский

Для ENNReal, c < a / b эквивалентно c b < a при подходящих условиях.

LaTeX

$$(hb0 : b \neq 0 \lor c \neq \infty) \land (hbt : b \neq \infty \lor c \neq 0) \implies c < \dfrac{a}{b} \iff c b < a$$

Lean4

protected theorem lt_div_iff_mul_lt (hb0 : b ≠ 0 ∨ c ≠ ∞) (hbt : b ≠ ∞ ∨ c ≠ 0) : c < a / b ↔ c * b < a :=
  lt_iff_lt_of_le_iff_le (ENNReal.div_le_iff_le_mul hb0 hbt)

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