no goals
α : Type u_1
β : Type ?u.13544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
⊢ Tendsto (fun p => insertNth (n + 1) p.fst p.snd) (𝓝 a ×ˢ 𝓝 []) (𝓝 (insertNth (n + 1) a []))
simp
α : Type u_1
β : Type ?u.13544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto ((fun p => insertNth (n + 1) p.fst p.snd) ∘ fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
    (𝓝 (insertNth (n + 1) a (a' :: l)))
α : Type u_1
β : Type ?u.13544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto (fun p => insertNth (n + 1) p.fst p.snd) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 (insertNth (n + 1) a (a' :: l)))
rw [this, tendsto_map'_iff]
no goals
α : Type u_1
β : Type ?u.13544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
⊢ Tendsto ((fun p => insertNth (n + 1) p.fst p.snd) ∘ fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
    (𝓝 (insertNth (n + 1) a (a' :: l)))
exact
  (tendsto_fst.comp tendsto_snd).cons
    ((@tendsto_insertNth' _ n l).comp <| tendsto_fst.prod_mk <| tendsto_snd.comp tendsto_snd)
α : Type u_1
β : Type ?u.13544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
⊢ (Seq.seq (Prod.mk <$> 𝓝 a) fun x => Seq.seq (cons <$> 𝓝 a') fun x => 𝓝 l) =
    (fun p => (p.fst, p.snd.fst :: p.snd.snd)) <$>
      Seq.seq (Prod.mk <$> 𝓝 a) fun x => Seq.seq (Prod.mk <$> 𝓝 a') fun x => 𝓝 l
α : Type u_1
β : Type ?u.13544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
n : ℕ
a' : α
l : List α
⊢ 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.fst, p.snd.fst :: p.snd.snd)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)
simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]