tsum_comp_le_tsum_of_injective — Mathlib

English

If f: α → β is injective, then for any g: β → ℝ≥0∞, ∑' x g(f(x)) ≤ ∑' y g(y).

Русский

Если f: α → β инъективна, то для любой g: β → ℝ≥0∞ выполняется ∑' x g(f(x)) ≤ ∑' y g(y).

LaTeX

$$$\sum' x, g(f(x)) \le \sum' y, g(y).$$$

Lean4

theorem tsum_comp_le_tsum_of_injective {f : α → β} (hf : Injective f) (g : β → ℝ≥0∞) : ∑' x, g (f x) ≤ ∑' y, g y :=
  ENNReal.summable.tsum_le_tsum_of_inj f hf (fun _ _ => zero_le _) (fun _ => le_rfl) ENNReal.summable

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