trop_iInf — Mathlib

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]

Похожие утверждения