α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.149530
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto (fun x => (restrict s f x.fst, restrict s f x.snd)) (𝓤 ↑s) (𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.149530
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ UniformContinuous (restrict s f)
delta UniformContinuousOn UniformContinuous
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.149530
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x => (f x.fst, f x.snd)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x => (restrict s f x.fst, restrict s f x.snd)) (𝓤 ↑s) (𝓤 β)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.149530
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto (fun x => (f x.fst, f x.snd)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto (fun x => (restrict s f x.fst, restrict s f x.snd)) (𝓤 ↑s) (𝓤 β)
rw [← map_uniformity_set_coe, tendsto_map'_iff]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.149530
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x => (f x.fst, f x.snd)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x => (restrict s f x.fst, restrict s f x.snd)) (𝓤 ↑s) (𝓤 β)
rfl