mathlib

2f4f8ad4 - feat(set_theory/principal): Principal ordinals are unbounded (#11755)

feat(set_theory/principal): Principal ordinals are unbounded (#11755) Amazingly, this theorem requires no conditions on the operation. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>