α : Type ?u.1666
inst✝ : TopologicalSpace α
⊢ OrdConnected (Ioo ⊥ ⊤)
α : Type ?u.1666
inst✝ : TopologicalSpace α
⊢ OrdConnected (range Real.toEReal)
rw [range_coe_eq_Ioo]
no goals
α : Type ?u.1666
inst✝ : TopologicalSpace α
⊢ OrdConnected (Ioo ⊥ ⊤)
exact ordConnected_Ioo