α : Type ?u.1479
β : Type ?u.1482
γ : Type ?u.1485
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ OrdConnected (Iio ⊤)
α : Type ?u.1479
β : Type ?u.1482
γ : Type ?u.1485
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ OrdConnected (range some)
rw [range_coe']
no goals
α : Type ?u.1479
β : Type ?u.1482
γ : Type ?u.1485
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ OrdConnected (Iio ⊤)
exact ordConnected_Iio