α : Type u_1
β : Type ?u.64741
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : Vector α n
⊢ Tendsto (fun x => ↑(x.fst ::ᵥ x.snd)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: ↑l))
α : Type u_1
β : Type ?u.64741
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : Vector α n
⊢ Tendsto (fun p => p.fst ::ᵥ p.snd) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l))
rw [tendsto_subtype_rng, cons_val]
no goals
α : Type u_1
β : Type ?u.64741
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : Vector α n
⊢ Tendsto (fun x => ↑(x.fst ::ᵥ x.snd)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: ↑l))
exact tendsto_fst.cons (Tendsto.comp continuousAt_subtype_val tendsto_snd)