α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.156682
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (fun x => ((f₁ x.fst, f₂ x.fst), f₁ x.snd, f₂ x.snd)) (𝓤 α)
    (comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 β) ⊓ comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 γ))
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.156682
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ UniformContinuous fun a => (f₁ a, f₂ a)
rw [UniformContinuous, uniformity_prod]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.156682
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (fun x => ((f₁ x.fst, f₂ x.fst), f₁ x.snd, f₂ x.snd)) (𝓤 α)
    (comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 β) ⊓ comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 γ))
exact tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩