toMulLeftMono — Mathlib

English

Multiplication on the left preserves order: if a ≤ b then c · a ≤ c · b for all c.

Русский

Умножение слева сохраняет порядок: если a ≤ b, то для всех c выполняется c · a ≤ c · b.

LaTeX

$$$\forall a,b,c \in \alpha,\ a \le b \Rightarrow c \cdot a \le c \cdot b$$$

Lean4

instance (priority := 100) toMulLeftMono : MulLeftMono α :=
  ⟨fun a b c hbc ↦ add_eq_left_iff_le.1 <| by rw [← mul_add, hbc.add_eq_left]⟩
    -- See note [lower instance priority]

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