mathlib

8da9e305 - chore(set_theory/ordinal/initial_seg): swap the names of `init` and `init'` (#18534)

chore(set_theory/ordinal/initial_seg): swap the names of `init` and `init'` (#18534) The former `init` was stated with the non-preferred `to_embedding` spelling, and the primed `init'` used `coe_fn`. Swapping them around is consistent with how most other bundled morphisms are handled. mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/2581