α : Type u
β : Type v
γ : Type ?u.284993
δ : Type ?u.284996
ε : Type ?u.284999
ζ : Type ?u.285002
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.285013
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
x : (a : ι) → π a
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → s a ∈ 𝓝 (x a)
⊢ ∀ (i_1 : ι), i_1 ∈ i → eval i_1 ⁻¹' s i_1 ∈ 𝓝 x
α : Type u
β : Type v
γ : Type ?u.284993
δ : Type ?u.284996
ε : Type ?u.284999
ζ : Type ?u.285002
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.285013
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
x : (a : ι) → π a
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → s a ∈ 𝓝 (x a)
⊢ Set.pi i s ∈ 𝓝 x
rw [pi_def, biInter_mem hi]
no goals
α : Type u
β : Type v
γ : Type ?u.284993
δ : Type ?u.284996
ε : Type ?u.284999
ζ : Type ?u.285002
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.285013
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
i : Set ι
s : (a : ι) → Set (π a)
x : (a : ι) → π a
hi : Set.Finite i
hs : ∀ (a : ι), a ∈ i → s a ∈ 𝓝 (x a)
⊢ ∀ (i_1 : ι), i_1 ∈ i → eval i_1 ⁻¹' s i_1 ∈ 𝓝 x
exact fun a ha => (continuous_apply a).continuousAt (hs a ha)