instAddMonoidWithOneTropical — Mathlib

English

For tropical x,y,z, x + y = z iff (x = z ∧ x ≤ y) ∨ (y = z ∧ y ≤ x).

Русский

Для тропических x,y,z, x+y=z тогда и только тогда, если (x=z ∧ x≤y) или (y=z ∧ y≤x).

LaTeX

$$$x + y = z \\iff (x = z \\land x \\le y) \\lor (y = z \\land y \\le x)$$$

Lean4

instance instAddMonoidWithOneTropical [LinearOrder R] [OrderTop R] [Zero R] : AddMonoidWithOne (Tropical R) :=
  { instOneTropical,
    instAddCommMonoidTropical with
    natCast := fun n => if n = 0 then 0 else 1
    natCast_zero := rfl
    natCast_succ := fun n => (untrop_inj_iff _ _).1 (by cases n <;> simp) }

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