lt_div_iff — Mathlib

English

Let a, b, c ∈ EReal with b > 0 and b ≠ ⊤. Then a < c / b if and only if a · b < c.

Русский

Пусть a, b, c ∈ EReal, b > 0 и b ≠ ⊤. Тогда a < c / b тогда и только тогда, когда a · b < c.

LaTeX

$$$a < \dfrac{c}{b} \iff a \cdot b < c \quad(0 < b,\; b \neq \top)$$

Lean4

theorem lt_div_iff (h : 0 < b) (h' : b ≠ ⊤) : a < c / b ↔ a * b < c :=
  by
  nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h)]
  rw [EReal.mul_div b a b, mul_comm a b]
  exact (strictMono_div_right_of_pos h h').lt_iff_lt

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