mathlib

e66e1f30 - feat(set_theory): add to cardinal, ordinal, cofinality (#963)

feat(set_theory): add to cardinal, ordinal, cofinality (#963) * feat(set_theory): add to cardinal, ordinal, cofinality The main new fact is the infinite pigeonhole principle Also includes many basic additions * fix name change in other files * address all of Mario's comments * use classical tactic in order/basic I did not use it for well_founded.succ, because that resulted in an error in lt_succ * fix error