mul_le_mul_of_mul_div_le — Mathlib

English

Let a, b, c, d be elements of a semifield with c > 0. If a · (b / c) ≤ d, then a · b ≤ d · c (equivalently, b · a ≤ d · c).

Русский

Пусть a, b, c, d — элементы полей с порядком, причём c > 0. Если a · (b / c) ≤ d, тогда a · b ≤ d · c (то есть b · a ≤ d · c).

LaTeX

$$$ (c > 0) \land \left(a \cdot \frac{b}{c} \le d\right) \Rightarrow ab \le dc $$$

Lean4

theorem mul_le_mul_of_mul_div_le (h : a * (b / c) ≤ d) (hc : 0 < c) : b * a ≤ d * c :=
  by
  rw [← mul_div_assoc] at h
  rwa [mul_comm b, ← div_le_iff₀ hc]

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