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