α : Type u
β : Type v
γ : Type ?u.284474
δ : Type ?u.284477
ε : Type ?u.284480
ζ : Type ?u.284483
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.284494
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
s : (i : ι) → Set (π i)
a : (i : ι) → π i
hs : Set.pi I s ∈ Filter.pi fun i => 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
α : Type u
β : Type v
γ : Type ?u.284474
δ : Type ?u.284477
ε : Type ?u.284480
ζ : Type ?u.284483
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.284494
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
s : (i : ι) → Set (π i)
a : (i : ι) → π i
hs : Set.pi I s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
rw [nhds_pi] at hs
no goals
α : Type u
β : Type v
γ : Type ?u.284474
δ : Type ?u.284477
ε : Type ?u.284480
ζ : Type ?u.284483
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.284494
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
I : Set ι
s : (i : ι) → Set (π i)
a : (i : ι) → π i
hs : Set.pi I s ∈ Filter.pi fun i => 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)
exact mem_of_pi_mem_pi hs hi