α : Type ?u.21185
⊢ (⨅ (l : ℝ≥0) (_ : l ≠ ⊥), 𝓟 (Set.Iio l)) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Set.Iio a)
α : Type ?u.21185
⊢ (⨅ (l : ℝ≥0) (_ : ⊥ < l), 𝓟 (Set.Iio l)) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Set.Iio a)
simp only [bot_lt_iff_ne_bot]
no goals
α : Type ?u.21185
⊢ (⨅ (l : ℝ≥0) (_ : l ≠ ⊥), 𝓟 (Set.Iio l)) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Set.Iio a)
rfl