α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
h : ∀ (i : ι), UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
h : ∀ (i : ι), UniformContinuous f
⊢ UniformContinuous f
delta UniformContinuous
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
h : ∀ (i : ι), UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
rwa [iInf_uniformity, tendsto_iInf]