English
For Finset S and f: S → Tropical R, trop of the infimum over S equals the sum of trop(f i).
Русский
Для Finset S и отображения f: S → Tropical R, trop inf {i ∈ S} f(i) равен сумме trop(f i).
LaTeX
$$$\forall s \in \mathrm{Finset}\,S,\ \operatorname{trop}(\inf_{i\in s} f(i)) = \sum_{i \in s} \operatorname{trop}(f(i))$$$
Lean4
theorem trop_inf [LinearOrder R] [OrderTop R] (s : Finset S) (f : S → R) : trop (s.inf f) = ∑ i ∈ s, trop (f i) :=
by
convert Multiset.trop_inf (s.val.map f)
simp only [Multiset.map_map, Function.comp_apply]
rfl