English
Let s be a finite set of elements, B a finite set of Finsets of α, and for each a ∈ s the number of Finsets in B containing a is at most n. Then the sum over t ∈ B of |s ∩ t| is at most |s| · n.
Русский
Пусть s — конечное множество элементов, B — конечное множество Finset(α). Пусть для каждого a ∈ s количество Finset в B, содержащих a, не превосходит n. Тогда ∑_{t∈B} |s ∩ t| ≤ |s| · n.
LaTeX
$$$\\forall s:\\mathrm{Finset}(\\alpha),\\ B:\\mathrm Finset(\\mathrm{Finset}(\\alpha)),\\n\\: (\\forall a ∈ s, \\#\\{t ∈ B \\,|\, a ∈ t\\} ≤ n) \\\\to\\\\ (\\sum_{t ∈ B} #(s \\cap t)) ≤ |s| · n$$
Lean4
/-- If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n`
times how many they are. -/
theorem sum_card_inter_le (h : ∀ a ∈ s, #({b ∈ B | a ∈ b}) ≤ n) : (∑ t ∈ B, #(s ∩ t)) ≤ #s * n :=
by
refine le_trans ?_ (s.sum_le_card_nsmul _ _ h)
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
exact sum_comm.le
