α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.238827
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
g : β → γ
l : Filter γ
a : α
⊢ map g (𝓝 (f a)) ≤ l ↔ Tendsto g (𝓝 (f a)) l
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.238827
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
g : β → γ
l : Filter γ
a : α
⊢ Tendsto (g ∘ f) (𝓝 a) l ↔ Tendsto g (𝓝 (f a)) l
rw [Tendsto, ← map_map, hf.map_nhds_eq]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.238827
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : OpenEmbedding f
g : β → γ
l : Filter γ
a : α
⊢ map g (𝓝 (f a)) ≤ l ↔ Tendsto g (𝓝 (f a)) l
rfl