instPosMulMono — Mathlib

English

Multiplication by a positive rational preserves order: if p ≤ q then p r ≤ q r for r > 0.

Русский

Умножение на положительное число сохраняет порядок: если p ≤ q, то pr ≤ qr при r > 0.

LaTeX

$$$p \le q \land r > 0 \Rightarrow p r \le q r$$$

Lean4

instance instPosMulMono : PosMulMono ℚ where
  elim := fun r p q h => by
    simp only [mul_comm]
    simpa [sub_mul, sub_nonneg] using Rat.mul_nonneg (sub_nonneg.2 h) r.2

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