Commit 2022-12-16 03:25 a0eb3163

View on Github →

feat: port Order.Bounds.OrderIso (#1063) a59dad53320b73ef180174aae867addd707ef00e

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Bounds/OrderIso.lean

added theorem OrderIso.isGLB_image'

added theorem OrderIso.isGLB_image

added theorem OrderIso.isGLB_preimage'

added theorem OrderIso.isGLB_preimage

added theorem OrderIso.isLUB_image'

added theorem OrderIso.isLUB_image

added theorem OrderIso.isLUB_preimage'

added theorem OrderIso.isLUB_preimage

added theorem OrderIso.lowerBounds_image

added theorem OrderIso.upperBounds_image