div_le_of_le_mul₀ — Mathlib

English

One direction of div_le_of_le_mul₀: a / b ≤ c given a ≤ c * b with b≥0, c≥0.

Русский

Одна сторона div_le_of_le_mul₀: если a ≤ c b, тогда a / b ≤ c, при b≥0, c≥0.

LaTeX

$$$b \ge 0,\ c \ge 0,\ a \le c \cdot b \Rightarrow \dfrac{a}{b} \le c$$$

Lean4

/-- One direction of `div_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative). -/
theorem div_le_of_le_mul₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a / b ≤ c :=
  div_eq_mul_inv a _ ▸ mul_inv_le_of_le_mul₀ hb hc h

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