α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.snd, F' q.fst q.snd)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto (fun q => (Prod.map f f' q.snd, Prod.map (F q.fst.fst) (F' q.fst.snd) q.snd)) ((p ×ˢ q) ×ˢ p' ×ˢ q')
    (𝓤 (β × β'))
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : TendstoUniformlyOnFilter F f p p'
h' : TendstoUniformlyOnFilter F' f' q q'
⊢ TendstoUniformlyOnFilter (fun i => Prod.map (F i.fst) (F' i.snd)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')
rw [tendstoUniformlyOnFilter_iff_tendsto] at h h' ⊢
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.snd, F' q.fst q.snd)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto
    (((fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ∘ fun q =>
        (Prod.map f f' q.snd, Prod.map (F q.fst.fst) (F' q.fst.snd) q.snd)) ∘
      fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.snd, F' q.fst q.snd)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto (fun q => (Prod.map f f' q.snd, Prod.map (F q.fst.fst) (F' q.fst.snd) q.snd)) ((p ×ˢ q) ×ˢ p' ×ˢ q')
    (𝓤 (β × β'))
rw [uniformity_prod_eq_comap_prod, tendsto_comap_iff, ← map_swap4_prod, tendsto_map'_iff]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
q : Filter ι'
q' : Filter α'
h : Tendsto (fun q => (f q.snd, F q.fst q.snd)) (p ×ˢ p') (𝓤 β)
h' : Tendsto (fun q => (f' q.snd, F' q.fst q.snd)) (q ×ˢ q') (𝓤 β')
⊢ Tendsto
    (((fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ∘ fun q =>
        (Prod.map f f' q.snd, Prod.map (F q.fst.fst) (F' q.fst.snd) q.snd)) ∘
      fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd))
    ((p ×ˢ p') ×ˢ q ×ˢ q') (𝓤 β ×ˢ 𝓤 β')
convert h.prod_map h'