English
Let s be finite and f: S → Tropical(WithTop R). Then the untrop of the sum equals the infimum of the untrops over the image of s, i.e., untrop (∑_{i∈s} f(i)) = inf sInf (untrop ∘ f '' s).
Русский
Пусть s конечно, и f: S → Tropical(WithTop R). Тогда untrop суммы ∑_{i∈s} f(i) равен инфимума множества {untrop(f(i)) : i ∈ s}, то есть untrop (∑_{i∈s} f(i)) = inf {untrop(f(i)) : i ∈ s}.
LaTeX
$$$\operatorname{untrop}\left(\sum_{i \in s} f(i)\right) = \inf \{ \operatorname{untrop}(f(i)) : i \in s \}.$$$
Lean4
theorem untrop_sum_eq_sInf_image [ConditionallyCompleteLinearOrder R] (s : Finset S) (f : S → Tropical (WithTop R)) :
untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' s) :=
by
rcases s.eq_empty_or_nonempty with (rfl | h)
· simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]
· rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']
