English
If f: α → ℝ≥0 is summable and i: β → α is injective, then ∑ f(i x) ≤ ∑ f(x).
Русский
Если f: α → ℝ≥0 суммируема и i: β → α инъективно, то сумма по композиции f ∘ i не превосходит суммарную по f.
LaTeX
$$$\\\\forall f : \\\\alpha \\\\to \\\\mathbb{R}_{\\\\ge 0}, \\\\mathrm{Summable}(f) \\\\Rightarrow \\\\forall i : \\\\beta \\\\to \\\\alpha, \\\\mathrm{Injective}(i) \\\\Rightarrow \\sum' x, f(i x) \\\\le \\sum' x, f x$$$
Lean4
theorem tsum_comp_le_tsum_of_inj {β : Type*} {f : α → ℝ≥0} (hf : Summable f) {i : β → α} (hi : Function.Injective i) :
(∑' x, f (i x)) ≤ ∑' x, f x :=
(summable_comp_injective hf hi).tsum_le_tsum_of_inj i hi (fun _ _ => zero_le _) (fun _ => le_rfl) hf