α : Type u_1
β : Type u_2
γ : Type ?u.305005
δ : Type ?u.305008
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto (f ∘ Subtype.val) (𝓝 { val := a, property := h }) l ↔ Tendsto (restrict s f) (𝓝 { val := a, property := h }) l
α : Type u_1
β : Type u_2
γ : Type ?u.305005
δ : Type ?u.305008
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto f (𝓝[s] a) l ↔ Tendsto (restrict s f) (𝓝 { val := a, property := h }) l
rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.305005
δ : Type ?u.305008
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto (f ∘ Subtype.val) (𝓝 { val := a, property := h }) l ↔ Tendsto (restrict s f) (𝓝 { val := a, property := h }) l
rfl