finsum_one — Mathlib

English

For any set s, the finsum over i in s of 1 equals the cardinality of s.

Русский

Для любого множества s сумма единиц по всем элементам s равна мощности множества s.

LaTeX

$$$\\sum_{i \\in s} 1 = |s|$$$

Lean4

@[simp]
theorem finsum_one {s : Set α} : ∑ᶠ i ∈ s, 1 = s.ncard :=
  by
  obtain hs | hs := s.infinite_or_finite
  · rw [hs.ncard]
    by_cases h : 1 = 0
    · simp [h]
    · exact finsum_mem_eq_zero_of_infinite (by simpa [Function.support_const h])
  · simp [finsum_mem_eq_finite_toFinset_sum _ hs, Set.ncard_eq_toFinset_card s hs]

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