Commit 2026-09-04 11:59 34f98d05
View on Github →feat: cardinality of Ultrafilter (#41297)
We prove there are 2 ^ 2 ^ #α ultrafilters on an infinite type α. For completeness, we also provide the cardinality lemma when α is finite.
feat: cardinality of Ultrafilter (#41297)
We prove there are 2 ^ 2 ^ #α ultrafilters on an infinite type α. For completeness, we also provide the cardinality lemma when α is finite.