Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-02 21:22 64fd9f8c

View on Github →

feat(order/rel_iso): preimages of intervals under an order_iso (#5183)

Estimated changes

added theorem order_iso.preimage_Icc
added theorem order_iso.preimage_Ici
added theorem order_iso.preimage_Ico
added theorem order_iso.preimage_Iic
added theorem order_iso.preimage_Iio
added theorem order_iso.preimage_Ioc
added theorem order_iso.preimage_Ioi
added theorem order_iso.preimage_Ioo