no goals
α : Type ?u.48158
β : Type ?u.48161
γ : Type ?u.48164
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ (⨅ (l : ℝ≥0∞) (_ : ⊥ < l), 𝓟 (Iio l)) = ⨅ (a : ℝ≥0∞) (_ : a ≠ 0), 𝓟 (Iio a)
simp [pos_iff_ne_zero, Iio]