Topology on lists and vectors #
Equations
- instTopologicalSpaceList = TopologicalSpace.mkOfNhds (traverse nhds)
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 α}
:
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)
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 α) => List.insertNth n p.1 p.2) (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 α) => List.insertNth n p.1 p.2
theorem
List.tendsto_removeNth
{α : Type u_1}
[TopologicalSpace α]
{n : ℕ}
{l : List α}
:
Filter.Tendsto (fun (l : List α) => List.removeNth l n) (nhds l) (nhds (List.removeNth l n))
theorem
List.continuous_removeNth
{α : Type u_1}
[TopologicalSpace α]
{n : ℕ}
:
Continuous fun (l : List α) => 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)
Equations
- Vector.instTopologicalSpaceVector n = id inferInstance
theorem
Vector.tendsto_insertNth
{α : Type u_1}
[TopologicalSpace α]
{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 (Vector.insertNth a i l))
theorem
Vector.continuous_insertNth'
{α : Type u_1}
[TopologicalSpace α]
{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}
[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