trop_minimum — Mathlib

English

For any LinearOrder R and list l, trop of the minimum of l equals the sum of trop of elements mapped through WithTop.some.

Русский

Для линейного порядка R и списка l, trop минимума равен сумме trop элементов, отображённых через WithTop.some.

LaTeX

$$$\forall l \in \mathrm{List}(R),\ \operatorname{trop}(\min l) = \mathrm{sum}(\mathrm{map}(\operatorname{trop} \circ \mathrm{WithTop}.some, l))$$$

Lean4

theorem trop_minimum [LinearOrder R] (l : List R) : trop l.minimum = List.sum (l.map (trop ∘ WithTop.some)) := by
  induction l with
  | nil => simp
  | cons hd tl IH => simp [List.minimum_cons, ← IH]

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