Commit 2023-03-02 13:10 8da9e305
View on Github →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