English
For ENNReal, if b ≠ 0 or c ≠ ∞ and b ≠ ∞ or c ≠ 0, then a ≤ c / b ⇔ a b ≤ c.
Русский
Для ENNReal, если b ≠ 0 или c ≠ ∞ и b ≠ ∞ или c ≠ 0, то a ≤ c / b ⇔ a b ≤ c.
LaTeX
$$(b \neq 0 \lor c \neq \infty) \land (b \neq \infty \lor c \neq 0) \implies \left( a \le \frac{c}{b} \iff a b \le c \right)$$
Lean4
protected theorem le_div_iff_mul_le (h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ∞ ∨ c ≠ ∞) : a ≤ c / b ↔ a * b ≤ c :=
by
cases b with
| top =>
lift c to ℝ≥0 using ht.neg_resolve_left rfl
rw [div_top, nonpos_iff_eq_zero]
rcases eq_or_ne a 0 with (rfl | ha) <;> simp [*]
| coe b => ?_
rcases eq_or_ne b 0 with (rfl | hb)
· have hc : c ≠ 0 := h0.neg_resolve_left rfl
simp [div_zero hc]
· rw [← coe_ne_zero] at hb
rw [← ENNReal.mul_le_mul_right hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]
