addLeftStrictMono — Mathlib

English

Lex(α →₀ N) has AddLeftStrictMono structure: adding the same finsupp on the left preserves strict inequality.

Русский

У Lex(α →₀ N) есть свойство AddLeftStrictMono: добавление слева одного и того же элемента сохраняет строгое неравенство.

LaTeX

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

Lean4

instance addLeftStrictMono : AddLeftStrictMono (Lex (α →₀ N)) :=
  ⟨fun _ _ _ ⟨a, lta, ha⟩ ↦ ⟨a, fun j ja ↦ congr_arg _ (lta j ja), add_lt_add_left ha _⟩⟩

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