α : Type u
β : Type v
γ : Type ?u.257106
δ : Type ?u.257109
ε : Type ?u.257112
ζ : Type ?u.257115
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.257126
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hs : ∀ (a : ι), a ∈ i → IsClosed (s a)
⊢ IsClosed (⋂ (a : ι) (_ : a ∈ i), eval a ⁻¹' s a)
α : Type u
β : Type v
γ : Type ?u.257106
δ : Type ?u.257109
ε : Type ?u.257112
ζ : Type ?u.257115
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.257126
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hs : ∀ (a : ι), a ∈ i → IsClosed (s a)
⊢ IsClosed (Set.pi i s)
rw [pi_def]
no goals
α : Type u
β : Type v
γ : Type ?u.257106
δ : Type ?u.257109
ε : Type ?u.257112
ζ : Type ?u.257115
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.257126
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hs : ∀ (a : ι), a ∈ i → IsClosed (s a)
⊢ IsClosed (⋂ (a : ι) (_ : a ∈ i), eval a ⁻¹' s a)
exact isClosed_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)