addRightStrictMono — Mathlib

English

Lex(α →₀ N) is AddRightStrictMono: adding on the right preserves strict inequality.

Русский

Lex(α →₀ N) обладает AddRightStrictMono: добавление справа сохраняет строгое неравенство.

LaTeX

$$$\\forall f,g,h,\\ f < g \\Rightarrow f+h < g+h$$$

Lean4

instance addRightStrictMono : AddRightStrictMono (Lex (α →₀ N)) :=
  ⟨fun f _ _ ⟨a, lta, ha⟩ ↦ ⟨a, fun j ja ↦ congr_arg (· + ofLex f j) (lta j ja), add_lt_add_right ha _⟩⟩

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