α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145087
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145087
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ UniformContinuous f
delta UniformContinuous
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145087
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (⨅ (i : ↑u₁), 𝓤 α) (𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145087
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
rw [sInf_eq_iInf', iInf_uniformity]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145087
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (⨅ (i : ↑u₁), 𝓤 α) (𝓤 β)
exact tendsto_iInf' ⟨u, h₁⟩ hf