Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-29 06:51 cd6f2720

View on Github →

feat(order/*): a bunch of lemmas about order_iso (#8451)

Estimated changes

Modified src/data/equiv/basic.lean

Modified src/order/bounds.lean

added theorem order_iso.is_glb_image

added theorem order_iso.is_glb_preimage

added theorem order_iso.is_lub_image

added theorem order_iso.is_lub_preimage

Modified src/order/rel_iso.lean

added theorem order_iso.image_eq_preimage

added theorem order_iso.image_preimage

added theorem order_iso.image_symm_image

added theorem order_iso.le_symm_apply

added theorem order_iso.preimage_image

added theorem order_iso.preimage_symm_preimage

added theorem order_iso.symm_image_image

added theorem order_iso.symm_preimage_preimage

Modified src/order/semiconj_Sup.lean

added theorem is_order_right_adjoint.comp_order_iso

added theorem is_order_right_adjoint.order_iso_comp

modified theorem is_order_right_adjoint.right_mono

deleted theorem is_order_right_adjoint.unique