Commit 2023-12-23 07:20 08e759d8

View on Github →

feat: OrderIso between minimals and maximals (#9190) Also extracts some lemmas from minimals_image_of_rel_iff_rel and remove _on from maximals_image_of_rel_iff_rel_on to match the former. for [#9088](https://github.com/leanprover-community/mathlib4/pull/9088#discussion_r1434641111)

Estimated changes

Modified Mathlib/Order/Minimal.lean

added def OrderIso.mapMaximals

added def OrderIso.mapMinimals

added theorem OrderIso.map_mem_maximals

added def OrderIso.maximalsIsoMinimals

added def OrderIso.minimalsIsoMaximals

added theorem RelEmbedding.image_maximals_eq

added theorem RelEmbedding.image_minimals_eq

deleted theorem RelEmbedding.maximals_image_eq

deleted theorem RelEmbedding.minimals_image_eq

added theorem image_maximals_of_rel_iff_rel

added theorem image_maximals_univ

added theorem image_minimals_of_rel_iff_rel

added theorem image_minimals_univ

added theorem map_mem_maximals

added theorem map_mem_maximals_iff

added theorem map_mem_minimals

added theorem map_mem_minimals_iff

deleted theorem maximals_image_of_rel_iff_rel_on

deleted theorem minimals_image_of_rel_iff_rel