Commit 2024-11-11 15:53 4328a7b6

View on Github →

chore(SetTheory/Ordinal/Basic): tweak preimage lemmas (#18061) We move the misplaced type_preimage next to its generalization type_lift_preimage, and reinstantiate the latter's simp attribute.

Estimated changes

modified theorem Ordinal.type_lift_preimage
modified theorem RelIso.ordinal_lift_type_eq