Commit 2022-01-10 23:30 4e7e5a6e

View on Github →

feat(set_theory/ordinal_arithmetic): Enumerating unbounded sets of ordinals with ordinals (#10979) This PR introduces enum_ord, which enumerates an unbounded set of ordinals using ordinals. This is used to build an explicit order isomorphism enum_ord.order_iso.

Estimated changes

Modified src/set_theory/ordinal.lean

added theorem ordinal.not_lt_omin

Modified src/set_theory/ordinal_arithmetic.lean

added def ordinal.CNF

added theorem ordinal.blsub_le_enum_ord

added def ordinal.enum_ord.order_iso

added theorem ordinal.enum_ord.strict_mono

added theorem ordinal.enum_ord.surjective

added def ordinal.enum_ord

added theorem ordinal.enum_ord_def'

added theorem ordinal.enum_ord_def'_H

added theorem ordinal.enum_ord_def

added theorem ordinal.enum_ord_def_H

added theorem ordinal.enum_ord_mem

added theorem ordinal.enum_ord_range

added theorem ordinal.eq_enum_ord