Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-05 19:53 0b575206

View on Github →

feat(order/bounds): Image under an order_iso and upper_bounds commute (#9555)

Estimated changes

Modified src/order/bounds.lean

added theorem monotone.image_lower_bounds_subset_lower_bounds_image

added theorem monotone.image_upper_bounds_subset_upper_bounds_image

modified theorem order_iso.is_glb_image'

modified theorem order_iso.is_glb_image

modified theorem order_iso.is_glb_preimage'

modified theorem order_iso.is_glb_preimage

modified theorem order_iso.is_lub_image'

modified theorem order_iso.is_lub_image

modified theorem order_iso.is_lub_preimage'

modified theorem order_iso.is_lub_preimage

added theorem order_iso.lower_bounds_image

added theorem order_iso.upper_bounds_image

Modified src/order/galois_connection.lean

deleted theorem order_iso.lower_bounds_image

deleted theorem order_iso.upper_bounds_image