case h
ι✝ : Type ?u.15394
α : Type u_2
β : Type ?u.15400
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_1
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ (i : ι), s i) ↔ x✝ ∈ ⋂ (i : ι), ↑(s i)
ι✝ : Type ?u.15394
α : Type u_2
β : Type ?u.15400
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_1
s : ι → Closeds α
⊢ ↑(⨅ (i : ι), s i) = ⋂ (i : ι), ↑(s i)
ext
no goals
case h
ι✝ : Type ?u.15394
α : Type u_2
β : Type ?u.15400
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_1
s : ι → Closeds α
x✝ : α
⊢ x✝ ∈ ↑(⨅ (i : ι), s i) ↔ x✝ ∈ ⋂ (i : ι), ↑(s i)
simp