inv_mul_le_of_le_mul₀ — Mathlib

English

If 0 ≤ b and 0 ≤ c and a ≤ b c, then b⁻¹ a ≤ c.

Русский

Пусть 0 ≤ b, 0 ≤ c и a ≤ b c, тогда b⁻¹ a ≤ c.

LaTeX

$$$$0 \le b \land 0 \le c \land a \le b c \Rightarrow b^{-1} a \le c.$$$$

Lean4

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

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