mathlib

fcceffa0 - chore(order/initial_seg): move definitions of initial and principal segments (#15328)

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)