α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : 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 β
i : ι
hf : UniformContinuous f
⊢ UniformContinuous f
delta UniformContinuous
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (⨅ (i : ι), 𝓤 α) (𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
rw [iInf_uniformity]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (⨅ (i : ι), 𝓤 α) (𝓤 β)
exact tendsto_iInf' i hf