mul_inv_le_of_le_mul₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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