α : Type ?u.22170
β : Type ?u.22173
γ : Type ?u.22176
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ IsOpen (Iio b)
α : Type ?u.22170
β : Type ?u.22173
γ : Type ?u.22176
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ IsOpen (Ico 0 b)
rw [ENNReal.Ico_eq_Iio]
no goals
α : Type ?u.22170
β : Type ?u.22173
γ : Type ?u.22176
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ IsOpen (Iio b)
exact isOpen_Iio