map_sum_eq_of_lt — Mathlib

English

If v x ≠ v y and v x > v y and a finite family sum with maximal term, the sum valuation equals the maximal term valuation.

Русский

Если v x ≠ v y и v x > v y, и сумма конечного набора имеет максимальный член, то оценка суммы равна оценке максимального члена.

LaTeX

$$$\\forall \\text{finite sum} \\; \\cdots \\Rightarrow v(\\sum) = \\max(v_\\text{max})$$$

Lean4

theorem map_sum_eq_of_lt {ι : Type*} {s : Finset ι} {f : ι → R} {j : ι} (hj : j ∈ s) (h0 : v (f j) ≠ 0)
    (hf : ∀ i ∈ s \ { j }, v (f i) < v (f j)) : v (∑ i ∈ s, f i) = v (f j) :=
  by
  rw [Finset.sum_eq_add_sum_diff_singleton hj]
  exact map_add_eq_of_lt_left _ (map_sum_lt _ h0 hf)

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