Commit 2024-08-26 10:46 d2c834ba

View on Github →

chore(SetTheory/Ordinal/*): make Ordinal.enum an order isomorphism (#5582) Suggested at https://github.com/leanprover-community/mathlib/pull/18547#discussion_r1149673778 Cons: This will cause goals of the form o ∈ {o : Ordinal | o < type r} rather than o < type r.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified def Ordinal.enum

deleted def Ordinal.enumIso

modified theorem Ordinal.enum_inj

modified theorem Ordinal.enum_le_enum'

modified theorem Ordinal.enum_le_enum

modified theorem Ordinal.enum_lt_enum

modified theorem Ordinal.one_out_eq

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

modified theorem Profinite.NobelingProof.Products.prop_of_isGood