English
For any finite set s and function f, if 0 < g and v(f(i)) < g for all i ∈ s, then v(∑_{i∈s} f(i)) < g.
Русский
Для любого конечного множества s и функции f, если 0 < g и v(f(i)) < g для всех i ∈ s, то v(∑_{i∈s} f(i)) < g.
LaTeX
$$$ 0 < g \,\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 : g ≠ 0) (hf : ∀ i ∈ s, v (f i) < g) :
v (∑ i ∈ s, f i) < g := by
classical
refine Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg)) (fun a s has ih hf => ?_) hf
rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
exact v.map_add_lt hf.1 (ih hf.2)
