le_sum_card — Mathlib

English

If α is finite and for all a ∈ α the number of B-fibers containing a is at least n, then |α| · n ≤ ∑_{s ∈ B} |s|.

Русский

Если α конечен и для всех a ∈ α число волокон B, содержащих a, не менее n, то |α|·n ≤ ∑_{s∈B} |s|.

LaTeX

$$$\\forall a,\\#\\{b ∈ B \\mid a ∈ b\\} ≥ n \\Longrightarrow |α| · n ≤ \\sum_{s ∈ B} |s|$$

Lean4

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

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