sum_card_le — Mathlib

English

If for every a in α the number of b in B with a ∈ b is at most n, then the sum over s ∈ B of s.card is at most |α| · n.

Русский

Если для каждого a ∈ α число b ∈ B с a ∈ b не превосходят n, то сумма по s∈B размера s.card не превосходит |α|·n.

LaTeX

$$$\\forall a,\\#\\{b ∈ B \\mid a ∈ b\\} ≤ n \\Longrightarrow \\sum_{s ∈ B} |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_le [Fintype α] (h : ∀ a, #({b ∈ B | a ∈ b}) ≤ n) : ∑ s ∈ B, #s ≤ Fintype.card α * n :=
  calc
    ∑ s ∈ B, #s = ∑ s ∈ B, #(univ ∩ s) := by simp_rw [univ_inter]
    _ ≤ Fintype.card α * n := sum_card_inter_le fun a _ ↦ h a

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