Commit 2024-01-23 11:19 75702221

View on Github →

feat: add lemmas about preimages of intervals under order embeddings (#9925) Also use them for Rat.cast.

Estimated changes

modified theorem Rat.preimage_cast_Icc
modified theorem Rat.preimage_cast_Ici
modified theorem Rat.preimage_cast_Ico
modified theorem Rat.preimage_cast_Iic
modified theorem Rat.preimage_cast_Iio
modified theorem Rat.preimage_cast_Ioc
modified theorem Rat.preimage_cast_Ioi
modified theorem Rat.preimage_cast_Ioo
added theorem Rat.preimage_cast_uIcc
added theorem Rat.preimage_cast_uIoc