exists_notMem_of_sum_card_lt
First moment method (counting form of the union bound): let S be a finite set and let B be a finite family of finite sets. If the sum of the cardinalities of the members of B is strictly less than the cardinality of S, then there is an element of S that belongs to no member of B.
Statement
theorem exists_notMem_of_sum_card_lt {α : Type*} [DecidableEq α] (S : Finset α) (B : Finset (Finset α)) (h : ∑ b ∈ B, b.card < S.card) : ∃ ω ∈ S, ∀ b ∈ B, ω ∉ b
- Source
- Alon & Spencer, The Probabilistic Method, Ch. 1 (the first moment method / union bound); Mathlib's `Finset.card_biUnion_le` and `Finset.card_le_card`.
- Verified
- 10 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Used by 1
- exists_two_coloring_of_card_mul_two_lt_two_powProperty B (Erdős). Let α be a finite set, let k ≥ 1, and let F be a finite family of subsets of α, each of cardinality at least k. If…
Read back from the Lean
For any type α with a decidable equality, and for any finset S : Finset α and any finset B : Finset (Finset α): if the sum, over all b ∈ B, of the cardinality of b is strictly less than the cardinality of S, then there exists an element ω with ω ∈ S such that for every b ∈ B, ω ∉ b. Explicitly, the quantifier structure is: ∀ α, [DecidableEq α] → ∀ S B, (∑ b ∈ B, b.card < S.card) → ∃ ω, ω ∈ S ∧ ∀ b, b ∈ B → ω ∉ b. In words: a family B of subsets (as finsets, hence without repetition) whose total sizes sum to less than |S| cannot cover S; some ω ∈ S lies outside every member of B. Note the inequality is strict, and the summation is over the elements b of the finset B (each counted once, weighted by its own cardinality), not over a multiset.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- First moment method: if the total size of a finite family of sets is less than `|S|`, some element of `S` avoids them all. -/ theorem exists_notMem_of_sum_card_lt {α : Type*} [DecidableEq α] (S : Finset α) (B : Finset (Finset α)) (h : ∑ b ∈ B, b.card < S.card) : ∃ ω ∈ S, ∀ b ∈ B, ω ∉ b := by by_contra hcon push Not at hcon have hsub : S ⊆ B.biUnion id := by intro ω hω obtain ⟨b, hb, hωb⟩ := hcon ω hω exact Finset.mem_biUnion.mpr ⟨b, hb, by simpa using hωb⟩ have h1 : S.card ≤ (B.biUnion id).card := Finset.card_le_card hsub have h2 : (B.biUnion id).card ≤ ∑ b ∈ B, b.card := Finset.card_biUnion_le linarith