Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.enum_inj

Modification history

2022-05-28 10:25

src/set_theory/ordinal/basic.lean

feat(set_theory/ordinal/basic): Turn various lemmas into `simp` (#14075)

Modified ordinal.enum_inj View on Github →

2022-03-03 16:19

src/set_theory/ordinal.lean

feat(set_theory/ordinal): `enum` is injective (#12319)

Added ordinal.enum_inj View on Github →