Topology on lists and vectors

instance instTopologicalSpaceList {α : Type u_1} [TopologicalSpace α] : TopologicalSpace (List α)

Equations

• instTopologicalSpaceList = TopologicalSpace.mkOfNhds (traverse nhds)

theorem nhds_list {α : Type u_1} [TopologicalSpace α] (as : List α) : nhds as = traverse nhds as

@[simp]

theorem nhds_nil {α : Type u_1} [TopologicalSpace α] : nhds [] = pure []

theorem nhds_cons {α : Type u_1} [TopologicalSpace α] (a : α) (l : List α) : nhds (a :: l) = List.cons <$> nhds a <*> nhds l

theorem List.tendsto_cons {α : Type u_1} [TopologicalSpace α] {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} [TopologicalSpace β] {α : Type u_3} {f : α → β} {g : α → List β} {a : Filter α} {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} [TopologicalSpace α] {β : Type u_3} {f : List α → β} {b : Filter β} {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} [TopologicalSpace α] : Continuous fun (x : α × List α) => x.1 :: x.2

theorem List.tendsto_nhds {α : Type u_1} [TopologicalSpace α] {β : Type u_3} {f : List α → β} {r : List α → Filter β} (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)

instance List.instDiscreteTopology {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] : DiscreteTopology (List α)

theorem List.continuousAt_length {α : Type u_1} [TopologicalSpace α] (l : List α) : ContinuousAt List.length l

theorem List.tendsto_insertIdx' {α : Type u_1} [TopologicalSpace α] {a : α} {n : ℕ} {l : List α} : Filter.Tendsto (fun (p : α × List α) => List.insertIdx n p.1 p.2) (nhds a ×ˢ nhds l) (nhds (List.insertIdx n a l))

Continuity of insertIdx in terms of Tendsto.

@[deprecated List.tendsto_insertIdx']

theorem List.tendsto_insertNth' {α : Type u_1} [TopologicalSpace α] {a : α} {n : ℕ} {l : List α} : Filter.Tendsto (fun (p : α × List α) => List.insertIdx n p.1 p.2) (nhds a ×ˢ nhds l) (nhds (List.insertIdx n a l))

Alias of List.tendsto_insertIdx'.

---

Continuity of insertIdx in terms of Tendsto.

theorem List.tendsto_insertIdx {α : Type u_1} [TopologicalSpace α] {β : Type u_3} {n : ℕ} {a : α} {l : List α} {f : β → α} {g : β → List α} {b : Filter β} (hf : Filter.Tendsto f b (nhds a)) (hg : Filter.Tendsto g b (nhds l)) : Filter.Tendsto (fun (b : β) => List.insertIdx n (f b) (g b)) b (nhds (List.insertIdx n a l))

@[deprecated List.tendsto_insertIdx']

theorem List.tendsto_insertNth {α : Type u_1} [TopologicalSpace α] {a : α} {n : ℕ} {l : List α} : Filter.Tendsto (fun (p : α × List α) => List.insertIdx n p.1 p.2) (nhds a ×ˢ nhds l) (nhds (List.insertIdx n a l))

Alias of List.tendsto_insertIdx'.

---

Continuity of insertIdx in terms of Tendsto.

theorem List.continuous_insertIdx {α : Type u_1} [TopologicalSpace α] {n : ℕ} : Continuous fun (p : α × List α) => List.insertIdx n p.1 p.2

@[deprecated List.continuous_insertIdx]

theorem List.continuous_insertNth {α : Type u_1} [TopologicalSpace α] {n : ℕ} : Continuous fun (p : α × List α) => List.insertIdx n p.1 p.2

Alias of List.continuous_insertIdx.

theorem List.tendsto_eraseIdx {α : Type u_1} [TopologicalSpace α] {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} [TopologicalSpace α] {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} [TopologicalSpace α] {n : ℕ} : Continuous fun (l : List α) => l.eraseIdx n

@[deprecated List.continuous_eraseIdx]

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

Alias of List.continuous_eraseIdx.

theorem List.tendsto_prod {α : Type u_1} [TopologicalSpace α] [Monoid α] [ContinuousMul α] {l : List α} : Filter.Tendsto List.prod (nhds l) (nhds l.prod)

theorem List.tendsto_sum {α : Type u_1} [TopologicalSpace α] [AddMonoid α] [ContinuousAdd α] {l : List α} : Filter.Tendsto List.sum (nhds l) (nhds l.sum)

theorem List.continuous_prod {α : Type u_1} [TopologicalSpace α] [Monoid α] [ContinuousMul α] : Continuous List.prod

theorem List.continuous_sum {α : Type u_1} [TopologicalSpace α] [AddMonoid α] [ContinuousAdd α] : Continuous List.sum

instance Vector.instTopologicalSpaceVector {α : Type u_1} [TopologicalSpace α] (n : ℕ) : TopologicalSpace (List.Vector α n)

Equations

• Vector.instTopologicalSpaceVector n = id inferInstance

theorem Vector.tendsto_cons {α : Type u_1} [TopologicalSpace α] {n : ℕ} {a : α} {l : List.Vector α n} : Filter.Tendsto (fun (p : α × List.Vector α n) => p.1 ::ᵥ p.2) (nhds a ×ˢ nhds l) (nhds (a ::ᵥ l))

theorem Vector.tendsto_insertIdx {α : Type u_1} [TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} {a : α} {l : List.Vector α n} : Filter.Tendsto (fun (p : α × List.Vector α n) => List.Vector.insertIdx p.1 i p.2) (nhds a ×ˢ nhds l) (nhds (List.Vector.insertIdx a i l))

@[deprecated List.tendsto_insertIdx']

theorem Vector.tendsto_insertNth {α : Type u_1} [TopologicalSpace α] {a : α} {n : ℕ} {l : List α} : Filter.Tendsto (fun (p : α × List α) => List.insertIdx n p.1 p.2) (nhds a ×ˢ nhds l) (nhds (List.insertIdx n a l))

Alias of List.tendsto_insertIdx'.

---

Continuity of insertIdx in terms of Tendsto.

theorem Vector.continuous_insertIdx' {α : Type u_1} [TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} : Continuous fun (p : α × List.Vector α n) => List.Vector.insertIdx p.1 i p.2

Continuity of Vector.insertIdx.

@[deprecated Vector.continuous_insertIdx']

theorem Vector.continuous_insertNth' {α : Type u_1} [TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} : Continuous fun (p : α × List.Vector α n) => List.Vector.insertIdx p.1 i p.2

Alias of Vector.continuous_insertIdx'.

---

Continuity of Vector.insertIdx.

theorem Vector.continuous_insertIdx {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {n : ℕ} {i : Fin (n + 1)} {f : β → α} {g : β → List.Vector α n} (hf : Continuous f) (hg : Continuous g) : Continuous fun (b : β) => List.Vector.insertIdx (f b) i (g b)

@[deprecated Vector.continuous_insertIdx]

theorem Vector.continuous_insertNth {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {n : ℕ} {i : Fin (n + 1)} {f : β → α} {g : β → List.Vector α n} (hf : Continuous f) (hg : Continuous g) : Continuous fun (b : β) => List.Vector.insertIdx (f b) i (g b)

Alias of Vector.continuous_insertIdx.

theorem Vector.continuousAt_eraseIdx {α : Type u_1} [TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} {l : List.Vector α (n + 1)} : ContinuousAt (List.Vector.eraseIdx i) l

@[deprecated Vector.continuousAt_eraseIdx]

theorem Vector.continuousAt_removeNth {α : Type u_1} [TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} {l : List.Vector α (n + 1)} : ContinuousAt (List.Vector.eraseIdx i) l

Alias of Vector.continuousAt_eraseIdx.

theorem Vector.continuous_eraseIdx {α : Type u_1} [TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} : Continuous (List.Vector.eraseIdx i)

@[deprecated Vector.continuous_eraseIdx]

theorem Vector.continuous_removeNth {α : Type u_1} [TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} : Continuous (List.Vector.eraseIdx i)

Alias of Vector.continuous_eraseIdx.