α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.149761
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x => f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (map Subtype.val (𝓝 { val := a, property := (_ : a ∈ s) })) (𝓝 (f a))
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.149761
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x => f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
rw [(@map_nhds_subtype_coe_eq_nhds α _ s a (mem_of_mem_nhds ha) ha).symm]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.149761
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x => f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (map Subtype.val (𝓝 { val := a, property := (_ : a ∈ s) })) (𝓝 (f a))
exact tendsto_map' hf.continuous.continuousAt