Commit 2024-08-29 12:34 923cc7a9

View on Github →

feat(Order/*): CovBy and OrderIso (#16222) We show that order isomorphisms map maximum elements, the covering relation, and successors.

Estimated changes

Modified Mathlib/Order/Cover.lean

added theorem OrderEmbedding.covBy_of_apply

added theorem OrderEmbedding.wcovBy_of_apply

added theorem OrderIso.map_covBy

added theorem OrderIso.map_wcovBy

Modified Mathlib/Order/Hom/Basic.lean

added theorem OrderIso.isMax_apply

added theorem OrderIso.isMin_apply

Modified Mathlib/Order/SuccPred/Basic.lean

added theorem OrderIso.map_pred

added theorem OrderIso.map_succ