Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-25 11:06 7c3269ca

View on Github →

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

Estimated changes

modified theorem pequiv.ext
modified theorem pequiv.ext_iff
added theorem initial_seg.ext