no goals
α : Type ?u.30563
β : Type ?u.30566
γ : Type ?u.30569
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
⊢ (⨅ (l : ℝ≥0∞) (_ : l < ⊤), 𝓟 (Ioi l)) = ⨅ (a : ℝ≥0∞) (_ : a ≠ ⊤), 𝓟 (Ioi a)
simp [lt_top_iff_ne_top, Ioi]