map_sum_le — Mathlib

English

If Ne g 0 and each v(f(i)) < g for i ∈ s, then v(∑_{i∈s} f(i)) < g.

Русский

Если g ≠ 0 и для каждого i ∈ s выполняется v(f(i)) < g, то v(∑_{i∈s} f(i)) < 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_le {ι : Type*} {s : Finset ι} {f : ι → R} {g : Γ₀} (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_le') (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_le hf.1 (ih hf.2)

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