English
For any Finset s and any f: S → Tropical (WithTop R) in a ConditionallyCompleteLinearOrder setting, the untrop of the sum equals the infimum over i : s of untrop (f i).
Русский
Для любой Finset s и функции f: S → Tropical(WithTop R) в рамках условной полноты линейного порядка, untrop суммы равен infimum по i : s от untrop (f i).
LaTeX
$$$\operatorname{untrop}\left(\sum_{i \in s} f(i)\right) = \inf_{i : s} \operatorname{untrop}(f(i)).$$$
Lean4
/-- Note we cannot use `i ∈ s` instead of `i : s` here
as it is simply not true on conditionally complete lattices! -/
theorem untrop_sum [ConditionallyCompleteLinearOrder R] (s : Finset S) (f : S → Tropical (WithTop R)) :
untrop (∑ i ∈ s, f i) = ⨅ i : s, untrop (f i) := by simpa [← _root_.untrop_sum] using (sum_attach _ _).symm
