Commit 2026-01-20 01:13 f760e25e

View on Github →

feat(NNReal): add lemmas about images of intervals (#34126)

Estimated changes

added theorem NNReal.image_coe_Icc
added theorem NNReal.image_coe_Ici
added theorem NNReal.image_coe_Ico
added theorem NNReal.image_coe_Iic
added theorem NNReal.image_coe_Iio
added theorem NNReal.image_coe_Ioc
added theorem NNReal.image_coe_Ioi
added theorem NNReal.image_coe_Ioo
added theorem NNReal.image_coe_uIcc
added theorem NNReal.image_coe_uIoc
added theorem NNReal.image_coe_uIoo
added theorem NNReal.range_coe