untrop_prod — Mathlib

English

For Finset S and f: S → Tropical R, untrop of the product equals the sum of untrops.

Русский

Для конечного множества S и отображения f: S → Tropical R, untrop произведения равен сумме untrop по элементам.

LaTeX

$$$\forall s \in \mathrm{Finset}\,S,\ \operatorname{untrop}\Big(\prod_{i \in s} f(i)\Big) = \sum_{i \in s} \operatorname{untrop}(f(i))$$$

Lean4

theorem untrop_prod [AddCommMonoid R] (s : Finset S) (f : S → Tropical R) :
    untrop (∏ i ∈ s, f i) = ∑ i ∈ s, untrop (f i) :=
  by
  convert Multiset.untrop_prod (s.val.map f)
  simp only [Multiset.map_map, Function.comp_apply]
  rfl

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