tsum_le_tsum_comp_of_surjective — Mathlib

English

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

Русский

Если f: α → β сюрьективна, то ∑' y g(y) ≤ ∑' x g(f(x)).

LaTeX

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

Lean4

theorem tsum_le_tsum_comp_of_surjective {f : α → β} (hf : Surjective f) (g : β → ℝ≥0∞) : ∑' y, g y ≤ ∑' x, g (f x) :=
  calc
    ∑' y, g y = ∑' y, g (f (surjInv hf y)) := by simp only [surjInv_eq hf]
    _ ≤ ∑' x, g (f x) := tsum_comp_le_tsum_of_injective (injective_surjInv hf) _

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