Commit 2024-05-01 14:27 d24a6580

View on Github →

feat(Order/Minimals, Order/RelIso/Set): four RelIso lemmas (#12558) This PR proves four rewrite lemmas about RelIso for statements that were previously a little awkward to navigate.

Estimated changes

Modified Mathlib/Order/Minimal.lean

added theorem RelIso.maximals_preimage_eq

added theorem RelIso.minimals_preimage_eq

Modified Mathlib/Order/RelIso/Set.lean

added theorem RelIso.image_eq_preimage_symm

added theorem RelIso.preimage_eq_image_symm