English
Let R be a linearly ordered set with a top element. For any finite set s and any function f: S → Tropical(R), the tropical untrop of the sum over s equals the infimum of the untrops of the summands. Equivalently, for all such s and f, untrop (∑ i∈s f(i)) = inf_{i∈s} untrop(f(i)).
Русский
Пусть R – линейно упорядоченное множество с верхней границей. Для любого конечного множества s и функции f: S → Tropical(R) тропическое untrop суммы ∑_{i∈s} f(i) равно инфимуму значений untrop(f(i)) по i∈s. То есть untrop(∑_{i∈s} f(i)) = inf_{i∈s} untrop(f(i)).
LaTeX
$$$\operatorname{untrop}\left(\sum_{i \in s} f(i)\right) = \inf_{i \in s} \operatorname{untrop}\bigl(f(i)\bigr).$$$
Lean4
theorem untrop_sum' [LinearOrder R] [OrderTop R] (s : Finset S) (f : S → Tropical R) :
untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f) :=
by
convert Multiset.untrop_sum (s.val.map f)
simp only [Multiset.map_map, Function.comp_apply, inf_def]
