add_le_add_left — Mathlib

English

Addition on Z√d is order-preserving: if a ≤ b then c + a ≤ c + b for any c in Z√d.

Русский

Сложение в Z√d сохраняет порядок: если a ≤ b, то для любого c верно c + a ≤ c + b.

LaTeX

$$$$\forall a,b,c \in \mathbb{Z}\sqrt{d},\; a \le b \Rightarrow c + a \le c + b.$$$$

Lean4

protected theorem add_le_add_left (a b : ℤ√d) (ab : a ≤ b) (c : ℤ√d) : c + a ≤ c + b :=
  show Nonneg _ by rw [add_sub_add_left_eq_sub]; exact ab

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