Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-19 06:33 8ea5598d

View on Github →

chore(set_theory/ordinal/basic): golf (#18547)

Estimated changes

Modified src/order/initial_seg.lean

added theorem principal_seg.apply_subrel_iso

added theorem principal_seg.subrel_iso_apply

Modified src/set_theory/ordinal/basic.lean

modified def ordinal.enum

modified def ordinal.typein.principal_seg