α : Type ?u.6443
inst✝ : TopologicalSpace α
⊢ OrdConnected (Ici 0)
α : Type ?u.6443
inst✝ : TopologicalSpace α
⊢ OrdConnected (range ENNReal.toEReal)
rw [range_coe_ennreal]
no goals
α : Type ?u.6443
inst✝ : TopologicalSpace α
⊢ OrdConnected (Ici 0)
exact ordConnected_Ici