initial_seg): use `fun_like`, `embedding_like` (#18198)

Commit

2 years ago

feat(data/pequiv,order/initial_seg): use `fun_like`, `embedding_like` (#18198) This is a backport of leanprover-community/mathlib4#1488.

Author

urkud

Parents