add_lt_add_left — Mathlib

English

If a < b then for any c, c + a < c + b; i.e., addition preserves strict order.

Русский

Если a < b, то для любого c выполняется c + a < c + b; сложение сохраняет строгий порядок.

LaTeX

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

Lean4

protected theorem add_lt_add_left (a b : ℤ√d) (h : a < b) (c) : c + a < c + b := fun h' =>
  h (Zsqrtd.le_of_add_le_add_left _ _ _ h')

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