α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145371
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
h : ∀ (u : UniformSpace β), u ∈ u₂ → UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145371
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
h : ∀ (u : UniformSpace β), u ∈ u₂ → UniformContinuous f
⊢ UniformContinuous f
delta UniformContinuous
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145371
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
h : ∀ (u : UniformSpace β), u ∈ u₂ → UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (⨅ (i : ↑u₂), 𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.145371
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
h : ∀ (u : UniformSpace β), u ∈ u₂ → 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.145371
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
h : ∀ (u : UniformSpace β), u ∈ u₂ → UniformContinuous f
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α) (⨅ (i : ↑u₂), 𝓤 β)
exact tendsto_iInf.mpr fun ⟨u, hu⟩ => h u hu