sum_card — Mathlib

English

If for all a ∈ α we have #({b ∈ B | a ∈ b}) = n, then ∑_{s ∈ B} #s = |α| · n.

Русский

Если для каждого a ∈ α верно #({b ∈ B | a ∈ b}) = n, тогда сумма по s∈B кардинальностей #s равна |α|·n.

LaTeX

$$$\\forall a,\\#\\{b ∈ B \\mid a ∈ b\\} = n \\Rightarrow \\sum_{s ∈ B} |s| = |α| · n$$

Lean4

/-- If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how
many they are. -/
theorem sum_card [Fintype α] (h : ∀ a, #({b ∈ B | a ∈ b}) = n) : ∑ s ∈ B, #s = Fintype.card α * n := by
  simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]

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