# Topology on lists and vectors #

instance instTopologicalSpaceList {α : Type u_1} [] :
Equations
• instTopologicalSpaceList =
theorem nhds_list {α : Type u_1} [] (as : List α) :
nhds as = traverse nhds as
@[simp]
theorem nhds_nil {α : Type u_1} [] :
nhds [] = pure []
theorem nhds_cons {α : Type u_1} [] (a : α) (l : List α) :
nhds (a :: l) = Seq.seq (List.cons <\$> nhds a) fun (x : Unit) => nhds l
theorem List.tendsto_cons {α : Type u_1} [] {a : α} {l : List α} :
Filter.Tendsto (fun (p : α × List α) => p.1 :: p.2) (nhds a ×ˢ nhds l) (nhds (a :: l))
theorem Filter.Tendsto.cons {β : Type u_2} [] {α : Type u_3} {f : αβ} {g : αList β} {a : } {b : β} {l : List β} (hf : Filter.Tendsto f a (nhds b)) (hg : Filter.Tendsto g a (nhds l)) :
Filter.Tendsto (fun (a : α) => f a :: g a) a (nhds (b :: l))
theorem List.tendsto_cons_iff {α : Type u_1} [] {β : Type u_3} {f : List αβ} {b : } {a : α} {l : List α} :
Filter.Tendsto f (nhds (a :: l)) b Filter.Tendsto (fun (p : α × List α) => f (p.1 :: p.2)) (nhds a ×ˢ nhds l) b
theorem List.continuous_cons {α : Type u_1} [] :
Continuous fun (x : α × List α) => x.1 :: x.2
theorem List.tendsto_nhds {α : Type u_1} [] {β : Type u_3} {f : List αβ} {r : List α} (h_nil : Filter.Tendsto f (pure []) (r [])) (h_cons : ∀ (l : List α) (a : α), Filter.Tendsto f (nhds l) (r l)Filter.Tendsto (fun (p : α × List α) => f (p.1 :: p.2)) (nhds a ×ˢ nhds l) (r (a :: l))) (l : List α) :
Filter.Tendsto f (nhds l) (r l)
theorem List.continuousAt_length {α : Type u_1} [] (l : List α) :
ContinuousAt List.length l
theorem List.tendsto_insertNth' {α : Type u_1} [] {a : α} {n : } {l : List α} :
Filter.Tendsto (fun (p : α × List α) => List.insertNth n p.1 p.2) (nhds a ×ˢ nhds l) (nhds ())
theorem List.tendsto_insertNth {α : Type u_1} [] {β : Type u_3} {n : } {a : α} {l : List α} {f : βα} {g : βList α} {b : } (hf : Filter.Tendsto f b (nhds a)) (hg : Filter.Tendsto g b (nhds l)) :
Filter.Tendsto (fun (b : β) => List.insertNth n (f b) (g b)) b (nhds ())
theorem List.continuous_insertNth {α : Type u_1} [] {n : } :
Continuous fun (p : α × List α) => List.insertNth n p.1 p.2
theorem List.tendsto_eraseIdx {α : Type u_1} [] {n : } {l : List α} :
Filter.Tendsto (fun (x : List α) => x.eraseIdx n) (nhds l) (nhds (l.eraseIdx n))
@[deprecated List.tendsto_eraseIdx]
theorem List.tendsto_removeNth {α : Type u_1} [] {n : } {l : List α} :
Filter.Tendsto (fun (x : List α) => x.eraseIdx n) (nhds l) (nhds (l.eraseIdx n))

Alias of List.tendsto_eraseIdx.

theorem List.continuous_eraseIdx {α : Type u_1} [] {n : } :
Continuous fun (l : List α) => l.eraseIdx n
@[deprecated]
theorem List.continuous_removeNth {α : Type u_1} [] {n : } :
Continuous fun (l : List α) => l.eraseIdx n

Alias of List.continuous_eraseIdx.

theorem List.tendsto_sum {α : Type u_1} [] [] [] {l : List α} :
Filter.Tendsto List.sum (nhds l) (nhds l.sum)
theorem List.tendsto_prod {α : Type u_1} [] [] [] {l : List α} :
Filter.Tendsto List.prod (nhds l) (nhds l.prod)
theorem List.continuous_sum {α : Type u_1} [] [] [] :
Continuous List.sum
theorem List.continuous_prod {α : Type u_1} [] [] [] :
Continuous List.prod
instance Vector.instTopologicalSpace {α : Type u_1} [] (n : ) :
Equations
• = id inferInstance
theorem Vector.tendsto_cons {α : Type u_1} [] {n : } {a : α} {l : Vector α n} :
Filter.Tendsto (fun (p : α × Vector α n) => p.1 ::ᵥ p.2) (nhds a ×ˢ nhds l) (nhds (a ::ᵥ l))
theorem Vector.tendsto_insertNth {α : Type u_1} [] {n : } {i : Fin (n + 1)} {a : α} {l : Vector α n} :
Filter.Tendsto (fun (p : α × Vector α n) => Vector.insertNth p.1 i p.2) (nhds a ×ˢ nhds l) (nhds ())
theorem Vector.continuous_insertNth' {α : Type u_1} [] {n : } {i : Fin (n + 1)} :
Continuous fun (p : α × Vector α n) => Vector.insertNth p.1 i p.2
theorem Vector.continuous_insertNth {α : Type u_1} {β : Type u_2} [] [] {n : } {i : Fin (n + 1)} {f : βα} {g : βVector α n} (hf : ) (hg : ) :
Continuous fun (b : β) => Vector.insertNth (f b) i (g b)
theorem Vector.continuousAt_eraseIdx {α : Type u_1} [] {n : } {i : Fin (n + 1)} {l : Vector α (n + 1)} :
@[deprecated]
theorem Vector.continuousAt_removeNth {α : Type u_1} [] {n : } {i : Fin (n + 1)} {l : Vector α (n + 1)} :

Alias of Vector.continuousAt_eraseIdx.

theorem Vector.continuous_eraseIdx {α : Type u_1} [] {n : } {i : Fin (n + 1)} :
@[deprecated]
theorem Vector.continuous_removeNth {α : Type u_1} [] {n : } {i : Fin (n + 1)} :

Alias of Vector.continuous_eraseIdx.