Topology on lists and vectors

@[instance_reducible]

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 : Tendsto f a (nhds b)) (hg : Tendsto g a (nhds l)) : 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 length l

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

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 : β) => (g b).insertIdx n (f b)) b (nhds (l.insertIdx n a))

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

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))

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

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

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

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

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

@[instance_reducible]

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

Equations

• List.Vector.instTopologicalSpace n = { IsOpen := List.Vector.instTopologicalSpace._aux_1 n, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

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

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

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

Continuity of Vector.insertIdx.

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

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

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