Commit 2024-10-22 17:17 2deff082
View on Github →chore(SetTheory/Cardinal/Cofinality): tweak universes of RelIso.cof_eq_lift (#18042)
For c : Cardinal.{u}, the simp-normal form of lift.{max u v} c is lift.{v} c.
Also, some drive-by golfing.
chore(SetTheory/Cardinal/Cofinality): tweak universes of RelIso.cof_eq_lift (#18042)
For c : Cardinal.{u}, the simp-normal form of lift.{max u v} c is lift.{v} c.
Also, some drive-by golfing.