map_add_eq_of_lt_right — Mathlib

English

For a finite sum, if a distinguished term has maximal valuation and is nonzero, then the valuation of the sum equals the valuation of that distinguished term.

Русский

Для конечной суммы, если особый член имеет наибольшую оценку и не равен нулю, то оценка суммы равна оценке этого члена.

LaTeX

$$$\\forall v:{\\valution(R,\\Gamma_0)},\\forall s:{\\text{Finset}}\\forall f:{\\text{ι} \\to R}, \\forall j:\\, ι,\\; j\\in s\\;→\\; v(s.sum (λ i, f i)) = v(f j)$ при определённых условиях$$

Lean4

theorem map_add_eq_of_lt_right (h : v x < v y) : v (x + y) = v y :=
  (v.map_add_of_distinct_val h.ne).trans (max_eq_right_iff.mpr h.le)

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