instAddCommMonoidTropical — Mathlib

English

The tropicalization map trop is monotone with respect to the preorder on R.

Русский

Тропизация trop монотонна относительно порядка на R.

LaTeX

$$$\\forall x,y\\in R,\\; x \\le y \\Rightarrow \\operatorname{trop}(x) \\le \\operatorname{trop}(y)$$$

Lean4

instance instAddCommMonoidTropical [OrderTop R] : AddCommMonoid (Tropical R) :=
  { instZeroTropical,
    instAddCommSemigroupTropical with
    zero_add := fun _ => untrop_injective (min_top_left _)
    add_zero := fun _ => untrop_injective (min_top_right _)
    nsmul := nsmulRec }

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