Erdős problem 497
How many antichains in are there? That is, how many families of subsets of are there such that, if is such a family and , then ?
Sources
FormalConjectures/ErdosProblems/
497.lean
Retained formal statement
How many antichains in are there? That is, how many families of subsets of are there such that, if is such a family and , then ?
Sperner's theorem states that . This is also known as Dedekind's problem. Resolved by Kleitman [Kl69], who proved that the number of such families is
∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ (n : ℕ), ↑(DedekindNumber.M' n) = 2 ^ ((1 + o n) * ↑(n.choose (n / 2)))