α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t, t ∈ 𝓝[s] x✝³ ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ x✝¹) ↔
    ∃ t, t ∈ 𝓝[s] x✝³ ∧ ∀ᶠ (x : ι) in p, ∀ (y : α), y ∈ t → (x, y) ∈ (fun y => (f y.snd, F y.fst y.snd)) ⁻¹' x✝¹
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t, t ∈ 𝓝[s] x✝³ ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ x✝¹) ↔
    x✝¹ ∈ map (fun y => (f y.snd, F y.fst y.snd)) (p ×ˢ 𝓝[s] x✝³)
rw [mem_map, mem_prod_iff_right]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t, t ∈ 𝓝[s] x✝³ ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ x✝¹) ↔
    ∃ t, t ∈ 𝓝[s] x✝³ ∧ ∀ᶠ (x : ι) in p, ∀ (y : α), y ∈ t → (x, y) ∈ (fun y => (f y.snd, F y.fst y.snd)) ⁻¹' x✝¹
rfl