untrop_sum — Mathlib

English

For AddMonoid R, untrop sum over Tropical R via a multiset equals the tropical sum.

Русский

Для AddMonoid R сумма Untrop по Tropical R через мультисет равна тропической сумме.

LaTeX

$$$\forall s \in \mathrm{Multiset}(\mathrm{Tropical}(R)),\ \operatorname{untrop}(s.sum) = \mathrm{sum}(\mathrm{map}\,\operatorname{untrop}\, s)$$$

Lean4

theorem untrop_sum [LinearOrder R] [OrderTop R] (s : Multiset (Tropical R)) :
    untrop s.sum = Multiset.inf (s.map untrop) := by
  induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp only [sum_cons, untrop_add, map_cons, inf_cons, ← IH]

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