mathlib documentation

topology.list

Topology on lists and vectors

theorem nhds_list {α : Type u_1} [topological_space α] (as : list α) :

theorem nhds_nil {α : Type u_1} [topological_space α] :

theorem nhds_cons {α : Type u_1} [topological_space α] (a : α) (l : list α) :

theorem list.tendsto_cons {α : Type u_1} [topological_space α] {a : α} {l : list α} :
filter.tendsto (λ (p : α × list α), p.fst :: p.snd) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a :: l))

theorem filter.tendsto.cons {β : Type u_2} [topological_space β] {α : Type u_1} {f : α → β} {g : α → list β} {a : filter α} {b : β} {l : list β} :
filter.tendsto f a (𝓝 b)filter.tendsto g a (𝓝 l)filter.tendsto (λ (a : α), f a :: g a) a (𝓝 (b :: l))

theorem list.tendsto_cons_iff {α : Type u_1} [topological_space α] {β : Type u_2} {f : list α → β} {b : filter β} {a : α} {l : list α} :
filter.tendsto f (𝓝 (a :: l)) b filter.tendsto (λ (p : α × list α), f (p.fst :: p.snd)) (𝓝 a ×ᶠ 𝓝 l) b

theorem list.continuous_cons {α : Type u_1} [topological_space α] :
continuous (λ (x : α × list α), x.fst :: x.snd)

theorem list.tendsto_nhds {α : Type u_1} [topological_space α] {β : Type u_2} {f : list α → β} {r : list αfilter β} (h_nil : filter.tendsto f (pure list.nil) (r list.nil)) (h_cons : ∀ (l : list α) (a : α), filter.tendsto f (𝓝 l) (r l)filter.tendsto (λ (p : α × list α), f (p.fst :: p.snd)) (𝓝 a ×ᶠ 𝓝 l) (r (a :: l))) (l : list α) :
filter.tendsto f (𝓝 l) (r l)

theorem list.tendsto_insert_nth' {α : Type u_1} [topological_space α] {a : α} {n : } {l : list α} :
filter.tendsto (λ (p : α × list α), list.insert_nth n p.fst p.snd) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (list.insert_nth n a l))

theorem list.tendsto_insert_nth {α : Type u_1} [topological_space α] {β : Type u_2} {n : } {a : α} {l : list α} {f : β → α} {g : β → list α} {b : filter β} :
filter.tendsto f b (𝓝 a)filter.tendsto g b (𝓝 l)filter.tendsto (λ (b : β), list.insert_nth n (f b) (g b)) b (𝓝 (list.insert_nth n a l))

theorem list.continuous_insert_nth {α : Type u_1} [topological_space α] {n : } :
continuous (λ (p : α × list α), list.insert_nth n p.fst p.snd)

theorem list.tendsto_remove_nth {α : Type u_1} [topological_space α] {n : } {l : list α} :
filter.tendsto (λ (l : list α), l.remove_nth n) (𝓝 l) (𝓝 (l.remove_nth n))

theorem list.continuous_remove_nth {α : Type u_1} [topological_space α] {n : } :
continuous (λ (l : list α), l.remove_nth n)

theorem list.tendsto_sum {α : Type u_1} [topological_space α] [add_monoid α] [has_continuous_add α] {l : list α} :

theorem list.tendsto_prod {α : Type u_1} [topological_space α] [monoid α] [has_continuous_mul α] {l : list α} :

theorem vector.tendsto_cons {α : Type u_1} [topological_space α] {n : } {a : α} {l : vector α n} :
filter.tendsto (λ (p : α × vector α n), p.fst::ᵥp.snd) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a::ᵥl))

theorem vector.tendsto_insert_nth {α : Type u_1} [topological_space α] {n : } {i : fin (n + 1)} {a : α} {l : vector α n} :

theorem vector.continuous_insert_nth' {α : Type u_1} [topological_space α] {n : } {i : fin (n + 1)} :
continuous (λ (p : α × vector α n), vector.insert_nth p.fst i p.snd)

theorem vector.continuous_insert_nth {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {n : } {i : fin (n + 1)} {f : β → α} {g : β → vector α n} :
continuous fcontinuous gcontinuous (λ (b : β), vector.insert_nth (f b) i (g b))

theorem vector.continuous_at_remove_nth {α : Type u_1} [topological_space α] {n : } {i : fin (n + 1)} {l : vector α (n + 1)} :

theorem vector.continuous_remove_nth {α : Type u_1} [topological_space α] {n : } {i : fin (n + 1)} :