Commit 2022-08-07 23:17 0e9c7c16

View on Github →

feat(order/initial_seg): exchange down and down' (#15802) As customary throughout mathlib, we prime the structure field, and unprime any theorem subsequently derived from it.

Estimated changes

Modified src/order/initial_seg.lean

deleted theorem principal_seg.down'

added theorem principal_seg.down

modified theorem principal_seg.lt_top

Modified src/set_theory/ordinal/basic.lean