Documentation

Mathlib.Topology.List

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 : 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 α] :

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

TopologicalSpace (Vector α n)

Equations

List.Vector.instTopologicalSpace n = id inferInstance

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)