div_lt_iff — Mathlib

English

Let a, b, c be ENNReal numbers with the conditions b ≠ 0 or c ≠ ∞ and b ≠ ∞ or c ≠ ∞. Then c/b < a if and only if c < a b.

Русский

Пусть a, b, c — элементы ENNReal, удовлетворяющие b ≠ 0 или c ≠ ∞ и b ≠ ∞ или c ≠ ∞. Тогда c/b < a тогда же, что и c < a b.

LaTeX

$$$\\left( b \\neq 0 \\\\lor \\\\ c \\neq \\infty \\right) \\\\land \\\\left( b \\neq \\infty \\lor c \\neq \\infty \\right) \\implies \\frac{c}{b} < a \\iff c < a b$$$

Lean4

protected theorem div_lt_iff (h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ∞ ∨ c ≠ ∞) : c / b < a ↔ c < a * b :=
  lt_iff_lt_of_le_iff_le <| ENNReal.le_div_iff_mul_le h0 ht

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