map_sum_lt' — Mathlib

English

Same as map_sum_lt with a nonzero bound: if g ≠ 0 and each v(f(i)) < g, then v(sum) < g.

Русский

То же, что и map_sum_lt: если g ≠ 0 и каждый v(f(i)) < g, то v(сумма) < g.

LaTeX

$$$ Ne(g, 0) \Rightarrow (\forall i \in s, v(f(i)) < g) \Rightarrow v\left(\sum_{i\in s} f(i)\right) < g $$$

Lean4

theorem map_sum_lt' {ι : Type*} {s : Finset ι} {f : ι → R} {g : Γ₀} (hg : 0 < g) (hf : ∀ i ∈ s, v (f i) < g) :
    v (∑ i ∈ s, f i) < g :=
  v.map_sum_lt (ne_of_gt hg) hf

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