α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V
set φ := fun q : α × β => ((x, q.2), q)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (fun q => (F x q.snd, F q.fst q.snd)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ TendstoUniformlyOn F (F x) (𝓝[U] x) V
rw [tendstoUniformlyOn_iff_tendsto]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (fun q => (F x q.snd, F q.fst q.snd)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
change Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ fun q => ((x, q.snd), q)) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V))
    (𝓤 γ)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
simp only [nhdsWithin, SProd.sprod, Filter.prod, comap_inf, inf_assoc, comap_principal,
  inf_principal]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (fun q => ((x, q.snd), q)) (comap Prod.fst (𝓝 x)) (𝓤 (α × β))
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (Prod.map (↿F) ↿F ∘ fun q => ((x, q.snd), q)) (comap Prod.fst (𝓝 x) ⊓ 𝓟 (Prod.fst ⁻¹' U ∩ Prod.snd ⁻¹' V))
    (𝓤 γ)
refine hF.comp (Tendsto.inf ?_ <| tendsto_principal_principal.2 <| fun x hx => ⟨⟨hU, hx.2⟩, hx⟩)
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F✝ : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
x : α
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q => ((x, q.snd), q)
⊢ Tendsto (fun x_1 => ((x, x_1.fst), x_1.snd, x_1.snd)) (comap (fun x_1 => (x, x_1.fst)) (𝓤 α)) (𝓤 α ×ˢ 𝓤 β)
exact tendsto_comap.prod_mk (tendsto_diag_uniformity _ _)