addLeftMono — Mathlib

English

Addition on the left is monotone in Tropical R: if x ≤ y, then x + z ≤ y + z for all z.

Русский

Сложение слева монотонно: если x ≤ y, то x + z ≤ y + z для всех z.

LaTeX

$$$\forall x,y,z \in \mathrm{Tropical}(R),\ x \le y \Rightarrow x + z \le y + z$$$

Lean4

instance addLeftMono [LinearOrder R] : AddLeftMono (Tropical R) :=
  ⟨fun x y z h => by
    rcases le_total x y with hx | hy
    · rw [add_eq_left hx, add_eq_left (hx.trans h)]
    · rw [add_eq_right hy]
      rcases le_total x z with hx | hx
      · rwa [add_eq_left hx]
      · rwa [add_eq_right hx]⟩

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