case h
α : Type ?u.132596
β : Type ?u.132599
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ (x ∈ ⋃ (n : ℕ), Iio ↑n) ↔ x ∈ {⊤}ᶜ
α : Type ?u.132596
β : Type ?u.132599
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ (⋃ (n : ℕ), Iio ↑n) = {⊤}ᶜ
ext x
case h
α : Type ?u.132596
β : Type ?u.132599
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {⊤}ᶜ
case h
α : Type ?u.132596
β : Type ?u.132599
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ (x ∈ ⋃ (n : ℕ), Iio ↑n) ↔ x ∈ {⊤}ᶜ
rw [mem_iUnion]
no goals
case h
α : Type ?u.132596
β : Type ?u.132599
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {⊤}ᶜ
exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩