case h
ι✝ : Type ?u.17060
α : Type u_2
β : Type ?u.17066
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_1
s : ι → Closeds α
⊢ ↑(⨅ (i : ι), s i) = ↑{ carrier := ⋂ (i : ι), ↑(s i), closed' := (_ : IsClosed (⋂ (i : ι), ↑(s i))) }
ι✝ : Type ?u.17060
α : Type u_2
β : Type ?u.17066
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_1
s : ι → Closeds α
⊢ (⨅ (i : ι), s i) = { carrier := ⋂ (i : ι), ↑(s i), closed' := (_ : IsClosed (⋂ (i : ι), ↑(s i))) }
ext1
no goals
case h
ι✝ : Type ?u.17060
α : Type u_2
β : Type ?u.17066
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Sort u_1
s : ι → Closeds α
⊢ ↑(⨅ (i : ι), s i) = ↑{ carrier := ⋂ (i : ι), ↑(s i), closed' := (_ : IsClosed (⋂ (i : ι), ↑(s i))) }
simp