le_sum_card_inter — Mathlib

English

If every a ∈ s belongs to at least n Finsets from B, then |s| · n ≤ ∑_{t ∈ B} |s ∩ t|.

Русский

Если каждый элемент a ∈ s принадлежит как минимум nFinset из B, тогда |s|·n ≤ ∑_{t∈B} |s∩t|.

LaTeX

$$$\\forall s: \\mathrm{Finset},\\ B: \\mathrm{Finset}(\\mathrm{Finset}(\\alpha)),\\n\\: (\\forall a ∈ s, n ≤ #(\\{b ∈ B \\mid a ∈ b\\})) \\\\to\\\\ #s · n ≤ \\sum_{t ∈ B} #(s \\cap t)$$

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_inter (h : ∀ a ∈ s, n ≤ #({b ∈ B | a ∈ b})) : #s * n ≤ ∑ t ∈ B, #(s ∩ t) :=
  by
  apply (s.card_nsmul_le_sum _ _ h).trans
  simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
  exact sum_comm.le

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