Commit 2025-03-23 13:52 831b7784

View on Github →

feat(ENNReal/Order): add images of intervals under (↑) : ℝ≥0 → ℝ≥0∞ (#23229)

Estimated changes

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