trop_inf — Mathlib

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

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