tsum_set_one — Mathlib

English

The sum over a set s of 1 equals the encard of s in ENNReal.

Русский

Сумма по множеству s единиц равна encard(s) в ENNReal.

LaTeX

$$$\sum'_{x \in s} 1 = s.encard$$

Lean4

theorem tsum_set_one : ∑' _ : s, (1 : ℝ≥0∞) = s.encard :=
  by
  obtain (hfin | hinf) := Set.finite_or_infinite s
  · lift s to Finset α using hfin
    simp [tsum_fintype]
  · have : Infinite s := infinite_coe_iff.mpr hinf
    rw [tsum_const_eq_top_of_ne_zero one_ne_zero, encard_eq_top hinf, ENat.toENNReal_top]

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