trop_inf — Mathlib

English

For Tropical R with LinearOrder and OrderTop, trop of the infimum of a multiset equals the sum of trop of the mapped elements.

Русский

Для Tropical R с линейным порядком и верхом trop inf множества равен сумме trop элементов.

LaTeX

$$$\forall s \in \mathrm{Multiset}(R),\ \operatorname{trop}(\inf s) = \mathrm{sum}(\mathrm{map}\,\operatorname{trop}\, s)$$$

Lean4

theorem trop_inf [LinearOrder R] [OrderTop R] (s : Multiset R) : trop s.inf = Multiset.sum (s.map trop) := by
  induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp [← IH]

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