no goals
α : Type ?u.872272
β : Type ?u.872275
s : Set ℝ
t : Set ℝ≥0
u : Set ℝ≥0∞
h : OrdConnected s
⊢ OrdConnected (ENNReal.ofReal '' s)
simpa only [image_image] using h.image_real_toNNReal.image_coe_nnreal_ennreal