α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x✝ : ℕ
⊢ Tendsto (fun l => removeNth l x✝) (pure []) (𝓝 (removeNth [] x✝))
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x✝ : ℕ
⊢ Tendsto (fun l => removeNth l x✝) (𝓝 []) (𝓝 (removeNth [] x✝))
rw [nhds_nil]
no goals
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x✝ : ℕ
⊢ Tendsto (fun l => removeNth l x✝) (pure []) (𝓝 (removeNth [] x✝))
exact tendsto_pure_nhds _ _
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Tendsto (fun p => removeNth (p.fst :: p.snd) 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 (removeNth (a :: l) 0))
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Tendsto (fun l => removeNth l 0) (𝓝 (a :: l)) (𝓝 (removeNth (a :: l) 0))
rw [tendsto_cons_iff]
no goals
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ Tendsto (fun p => removeNth (p.fst :: p.snd) 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 (removeNth (a :: l) 0))
exact tendsto_snd
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => removeNth (p.fst :: p.snd) (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (removeNth (a :: l) (n + 1)))
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : List α
⊢ Tendsto (fun l => removeNth l (n + 1)) (𝓝 (a :: l)) (𝓝 (removeNth (a :: l) (n + 1)))
rw [tendsto_cons_iff]
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => p.fst :: removeNth p.snd n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: removeNth l n))
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => removeNth (p.fst :: p.snd) (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 (removeNth (a :: l) (n + 1)))
dsimp [removeNth]
no goals
α : Type u_1
β : Type ?u.54838
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p => p.fst :: removeNth p.snd n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: removeNth l n))
exact tendsto_fst.cons ((@tendsto_removeNth n l).comp tendsto_snd)