Commit 2026-06-25 15:32 4364cadc

View on Github →

feat(Order/Hom/Basic): equivalences of Order{Hom/Embedding/Iso} (#38667)

OrderHoms are equivalent to RelHoms of LE (unlike OrderEmbedding/OrderIso they aren't defined using it)
Congruence equivs for OrderEmbedding/OrderIso when the two sides are order-isomorphic. This already exists for OrderHom.

Estimated changes

Modified Mathlib/Order/Hom/Basic.lean

added def OrderHom.equivRelHom

added theorem OrderIso.orderEmbeddingCongr_apply

added theorem OrderIso.orderEmbeddingCongr_symm_apply

added theorem OrderIso.orderIsoCongr_apply

added theorem OrderIso.orderIsoCongr_symm_apply