Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-03 12:53 2f4f8ad4

View on Github →

feat(set_theory/principal): Principal ordinals are unbounded (#11755) Amazingly, this theorem requires no conditions on the operation.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

deleted theorem ordinal.is_normal.lt_nfp

added theorem ordinal.lt_nfp

Modified src/set_theory/principal.lean

added def ordinal.blsub₂

added theorem ordinal.lt_blsub₂

added theorem ordinal.principal_nfp_blsub₂

added theorem ordinal.unbounded_principal