div_lt_iff — Mathlib

English

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

Русский

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

LaTeX

$$$0 < c \land c \neq \top \Rightarrow \dfrac{b}{c} < a \iff b < a c$$$

Lean4

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

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