English
Let p be a prime and s a finite set with F : s → ℚ. If for all i ∈ s we have |F(i)|_p ≤ t and t ≥ 0, then |∑_{i∈s} F(i)|_p ≤ t.
Русский
Пусть p — простое число и s — конечный набор с F : s → ℚ. Если для всех i ∈ s выполняется |F(i)|_p ≤ t и t ≥ 0, то |∑_{i∈s} F(i)|_p ≤ t.
LaTeX
$$$\\displaystyle \\forall \\alpha \\quad \\forall F:\\alpha \\to \\mathbb{Q}, \\quad \\forall s\\in\\mathrm{Finset}(\\alpha),\\quad \\forall t\\in\\mathbb{Q},\\quad t\\ge 0,\\quad (\\forall i\\in s,\\ |F(i)|_p \\le t) \\Rightarrow \\left|\\sum_{i\\in s} F(i)\\right|_p \\le t$$$
Lean4
theorem sum_le' {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α} (hF : ∀ i ∈ s, padicNorm p (F i) ≤ t) (ht : 0 ≤ t) :
padicNorm p (∑ i ∈ s, F i) ≤ t :=
by
obtain rfl | hs := Finset.eq_empty_or_nonempty s
· simp [ht]
· exact sum_le hs hF
