Commit 2022-12-15 21:39 cb8d5533

View on Github →

feat: port Order.Hom.Set (#1059) mathlib3 SHA: 198161d833f2c01498c39c266b0b3dbe2c7a8c07 porting notes: none

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Hom/Set.lean

added def OrderIso.Set.univ

added def OrderIso.compl

added theorem OrderIso.image_eq_preimage

added theorem OrderIso.image_preimage

added theorem OrderIso.image_symm_image

added theorem OrderIso.preimage_image

added theorem OrderIso.preimage_symm_preimage

added theorem OrderIso.range_eq

added def OrderIso.setCongr

added theorem OrderIso.symm_image_image

added theorem OrderIso.symm_preimage_preimage

added theorem StrictMono.coe_orderIsoOfSurjective

added theorem StrictMono.orderIsoOfSurjective_self_symm_apply

added theorem StrictMono.orderIsoOfSurjective_symm_apply_self

added theorem compl_antitone

added theorem compl_strictAnti