instMulLeftMono — Mathlib

English

Left multiplication by any fixed natural number is monotone: if x ≤ y, then a·x ≤ a·y for all a ∈ ℕ.

Русский

Левая операция умножения на фиксированное натуральное число монотонна: если x ≤ y, то a·x ≤ a·y для всех a ∈ ℕ.

LaTeX

$$$\forall a,x,y \in \mathbb{N},\ x \le y \Rightarrow a\cdot x \le a\cdot y.$$$

Lean4

instance instMulLeftMono : MulLeftMono ℕ where elim := fun _ _ _ h => mul_le_mul_left _ h

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