Commit 2022-07-17 15:25 fcceffa0

chore(order/initial_seg): move definitions of initial and principal segments (#15328) We move the definitions of initial and principal segments from set_theory/ordinal/basic.lean to a new file order/initial_seg.lean. We minimally change this file, just doing the following:

• add a copyright header
• copy over existing documentation
• add a few noncomputable attributes
• localize the notation
• use by_cases in initial_seg.lt_or_eq (needed as the classical locale is no longer open)