Commit 2024-10-22 17:17 3d42f39d

View on Github →

refactor(SetTheory/Ordinal/Basic): type_lt → type_toType (#18049) The new name is much more discoverable and makes clear that this isn't just any < relation.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Ordinal.type_toType