mul_le_of_le_mul_inv₀ — Mathlib

English

One direction of mul_le_mul_inv₀: if a ≤ c*b and b≥0, c≥0, then a*b^{-1} ≤ c.

Русский

Одна сторона mul_le_mul_inv₀: если a ≤ c b и b≥0, c≥0, то a b^{-1} ≤ c.

LaTeX

$$$b \ge 0,\ c \ge 0,\ a \le c \cdot b^{-1} \Rightarrow a \cdot b^{-1} \le c$$$

Lean4

/-- One direction of `le_mul_inv_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative).
-/
theorem mul_le_of_le_mul_inv₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b * c⁻¹) : a * c ≤ b :=
  by
  obtain rfl | hc := hc.eq_or_lt
  · simpa using hb
  · rwa [le_mul_inv_iff₀ hc] at h

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