English
Let R be a ConditionallyCompleteLinearOrder and S be finite with a Fintype structure. For any f: S → Tropical(WithTop R), untrop (∑_{i: S} f i) equals the infimum over i: S of untrop (f i).
Русский
Пусть R — линейно упорядоченное множество с условной полнотой; S — конечно текущее множество. Для любой f: S → Tropical(WithTop R) имеем untrop(∑_{i∈S} f(i)) = ⨅ i : S, untrop(f(i)).
LaTeX
$$$\operatorname{untrop}\left(\sum_{i: S} f(i)\right) = \bigwedge_{i: S} \operatorname{untrop}(f(i)).$$$
Lean4
theorem untrop_sum [ConditionallyCompleteLinearOrder R] [Fintype S] (f : S → Tropical (WithTop R)) :
untrop (∑ i : S, f i) = ⨅ i : S, untrop (f i) := by
rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]
