sum_card_inter — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall a ∈ s,\\#\\{b ∈ B \\mid a ∈ b\\} = n \\Rightarrow \\sum_{t ∈ B} #(s ∩ t) = #s \\cdot 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_inter (h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) = n) : (∑ t ∈ B, #(s ∩ t)) = #s * n :=
  (sum_card_inter_le fun a ha ↦ (h a ha).le).antisymm (le_sum_card_inter fun a ha ↦ (h a ha).ge)

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