Commit 2025-01-05 11:29 f82d0858

View on Github →

chore(SetTheory/Ordinal/Basic): {x // x < y} → Iio y (#20413)

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.type_subrel_lt

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified def Ordinal.enum

modified theorem Ordinal.enum_inj

modified theorem Ordinal.enum_le_enum'

modified theorem Ordinal.enum_le_enum

modified theorem Ordinal.enum_lt_enum