α : Type u
β : Type v
γ : Type ?u.220683
δ : Type ?u.220686
ε : Type ?u.220689
ζ : Type ?u.220692
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.220703
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → IsOpen (s a)
⊢ IsOpen (⋂ (a : ι) (_ : a ∈ i), eval a ⁻¹' s a)
α : Type u
β : Type v
γ : Type ?u.220683
δ : Type ?u.220686
ε : Type ?u.220689
ζ : Type ?u.220692
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.220703
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → IsOpen (s a)
⊢ IsOpen (Set.pi i s)
rw [pi_def]
no goals
α : Type u
β : Type v
γ : Type ?u.220683
δ : Type ?u.220686
ε : Type ?u.220689
ζ : Type ?u.220692
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.220703
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → IsOpen (s a)
⊢ IsOpen (⋂ (a : ι) (_ : a ∈ i), eval a ⁻¹' s a)
exact isOpen_biInter hi fun a ha => (hs _ ha).preimage (continuous_apply _)