English
For ConditionallyCompleteLinearOrder R and finite S, trop of the iInf over S equals the finite sum of trop(f i).
Русский
Для ConditionallyCompleteLinearOrder R и конечного S trop iInf по S равен сумме trop(f i) по S.
LaTeX
$$$\forall f : S \to WithTop(R),\ trop\big(\mathrm{iInf}\,f\big) = \sum_{i:\,S} \operatorname{trop}(f(i))$$$
Lean4
theorem trop_iInf [ConditionallyCompleteLinearOrder R] [Fintype S] (f : S → WithTop R) :
trop (⨅ i : S, f i) = ∑ i : S, trop (f i) := by rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]