Finset.untrop_sum

theorem Finset.untrop_sum : ∀ {R : Type u_1} {S : Type u_2} [inst : ConditionallyCompleteLinearOrder R] (s : Finset S) (f : S → Tropical (WithTop R)), (s.sum fun i => f i).untrop = ⨅ i, (f ↑i).untrop

This theorem is about the concept of unwrapping the sum operation in the context of tropical arithmetic over conditionally complete lattices. Specifically, given any type `R` that forms a conditionally complete linear order, a finite set `s` of another type `S`, and a function `f` mapping from `S` to the 'tropicalized' version of `WithTop R` (which adds an element `⊤` to `R`), the 'untrop' of the sum of `f i` for each `i` in `s` is the infimum (`⨅`) of 'untrop' of `f ↑i` for each `i`. Note that `i ∈ s` cannot be used in this context as it is not generally true for conditionally complete lattices.

More concisely: Given a conditionally complete lattice `R`, a type `S`, a function `f : S -> WithTop R`, and `s` a finite subset of `S`, the untropicalized sum of `f i` for all `i` in `s` equals the infimum of the untropicalized sums `f (↑i)` over all `i` in `s`.