ι✝ : Type ?u.22254
α : Type u_2
β : Type ?u.22260
γ : Type ?u.22263
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_1
x : α
s : ι → Opens α
⊢ x ∈ ↑(iSup s) ↔ ∃ i, x ∈ s i
ι✝ : Type ?u.22254
α : Type u_2
β : Type ?u.22260
γ : Type ?u.22263
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_1
x : α
s : ι → Opens α
⊢ x ∈ iSup s ↔ ∃ i, x ∈ s i
rw [← SetLike.mem_coe]
no goals
ι✝ : Type ?u.22254
α : Type u_2
β : Type ?u.22260
γ : Type ?u.22263
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Sort u_1
x : α
s : ι → Opens α
⊢ x ∈ ↑(iSup s) ↔ ∃ i, x ∈ s i
simp