Topology on lists and vectors #
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 => f (p.fst :: p.snd)) (nhds a ×ˢ nhds l) b
theorem
List.continuous_cons
{α : Type u_1}
[TopologicalSpace α]
:
Continuous fun x => x.fst :: x.snd
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 => f (p.fst :: p.snd)) (nhds a ×ˢ nhds l) (r (a :: l)))
(l : List α)
:
Filter.Tendsto f (nhds l) (r l)
theorem
List.continuousAt_length
{α : Type u_1}
[TopologicalSpace α]
(l : List α)
:
ContinuousAt List.length l
theorem
List.tendsto_insertNth'
{α : Type u_1}
[TopologicalSpace α]
{a : α}
{n : ℕ}
{l : List α}
:
Filter.Tendsto (fun p => List.insertNth n p.fst p.snd) (nhds a ×ˢ nhds l) (nhds (List.insertNth n a l))
theorem
List.tendsto_insertNth
{α : 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.insertNth n (f b) (g b)) b (nhds (List.insertNth n a l))
theorem
List.continuous_insertNth
{α : Type u_1}
[TopologicalSpace α]
{n : ℕ}
:
Continuous fun p => List.insertNth n p.fst p.snd
theorem
List.tendsto_removeNth
{α : Type u_1}
[TopologicalSpace α]
{n : ℕ}
{l : List α}
:
Filter.Tendsto (fun l => List.removeNth l n) (nhds l) (nhds (List.removeNth l n))
theorem
List.continuous_removeNth
{α : Type u_1}
[TopologicalSpace α]
{n : ℕ}
:
Continuous fun l => List.removeNth l n
theorem
List.tendsto_sum
{α : Type u_1}
[TopologicalSpace α]
[AddMonoid α]
[ContinuousAdd α]
{l : List α}
:
Filter.Tendsto List.sum (nhds l) (nhds (List.sum l))
theorem
List.tendsto_prod
{α : Type u_1}
[TopologicalSpace α]
[Monoid α]
[ContinuousMul α]
{l : List α}
:
Filter.Tendsto List.prod (nhds l) (nhds (List.prod l))
theorem
List.continuous_sum
{α : Type u_1}
[TopologicalSpace α]
[AddMonoid α]
[ContinuousAdd α]
:
Continuous List.sum
theorem
List.continuous_prod
{α : Type u_1}
[TopologicalSpace α]
[Monoid α]
[ContinuousMul α]
:
Continuous List.prod
instance
Vector.instTopologicalSpaceVector
{α : Type u_1}
[TopologicalSpace α]
(n : ℕ)
:
TopologicalSpace (Vector α n)
theorem
Vector.tendsto_insertNth
{α : Type u_1}
[TopologicalSpace α]
{n : ℕ}
{i : Fin (n + 1)}
{a : α}
{l : Vector α n}
:
Filter.Tendsto (fun p => Vector.insertNth p.fst i p.snd) (nhds a ×ˢ nhds l) (nhds (Vector.insertNth a i l))
theorem
Vector.continuous_insertNth'
{α : Type u_1}
[TopologicalSpace α]
{n : ℕ}
{i : Fin (n + 1)}
:
Continuous fun p => Vector.insertNth p.fst i p.snd
theorem
Vector.continuous_insertNth
{α : 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 => Vector.insertNth (f b) i (g b)
theorem
Vector.continuousAt_removeNth
{α : Type u_1}
[TopologicalSpace α]
{n : ℕ}
{i : Fin (n + 1)}
{l : Vector α (n + 1)}
:
ContinuousAt (Vector.removeNth i) l