α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
⊢ ∀ (x : ℕ → ι × α), Tendsto x atTop (l ×ˢ 𝓟 s) → Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ x) atTop (𝓤 β)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
⊢ TendstoUniformlyOn F f l s
rw [tendstoUniformlyOn_iff_tendsto, tendsto_iff_seq_tendsto]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto u atTop (l ×ˢ 𝓟 s)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
⊢ ∀ (x : ℕ → ι × α), Tendsto x atTop (l ×ˢ 𝓟 s) → Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ x) atTop (𝓤 β)
intro u hu
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto u atTop (l ×ˢ 𝓟 s)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
rw [tendsto_prod_iff'] at hu
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
h : TendstoUniformlyOn (fun n => F (u n).fst) f atTop s
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
specialize h (fun n => (u n).fst) hu.1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
h : Tendsto (fun q => (f q.snd, F (u q.fst).fst q.snd)) (atTop ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
h : TendstoUniformlyOn (fun n => F (u n).fst) f atTop s
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
rw [tendstoUniformlyOn_iff_tendsto] at h
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
l : Filter ι
inst✝ : IsCountablyGenerated l
u : ℕ → ι × α
hu : Tendsto (fun n => (u n).fst) atTop l ∧ Tendsto (fun n => (u n).snd) atTop (𝓟 s)
h : Tendsto (fun q => (f q.snd, F (u q.fst).fst q.snd)) (atTop ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto ((fun q => (f q.snd, F q.fst q.snd)) ∘ u) atTop (𝓤 β)
exact h.comp (tendsto_id.prod_mk hu.2)