topology.list

# Topology on lists and vectors #

@[protected, instance]
def list.topological_space {α : Type u_1}  :
Equations
theorem nhds_list {α : Type u_1} (as : list α) :
@[simp]
theorem nhds_nil {α : Type u_1}  :
theorem nhds_cons {α : Type u_1} (a : α) (l : list α) :
nhds (a :: l) = <*> nhds l
theorem list.tendsto_cons {α : Type u_1} {a : α} {l : list α} :
filter.tendsto (λ (p : α × list α), p.fst :: p.snd) ((nhds a).prod (nhds l)) (nhds (a :: l))
theorem filter.tendsto.cons {β : Type u_2} {α : Type u_1} {f : α → β} {g : α → list β} {a : filter α} {b : β} {l : list β} (hf : (nhds b)) (hg : (nhds l)) :
filter.tendsto (λ (a : α), f a :: g a) a (nhds (b :: l))
theorem list.tendsto_cons_iff {α : Type u_1} {β : Type u_2} {f : list α → β} {b : filter β} {a : α} {l : list α} :
(nhds (a :: l)) b filter.tendsto (λ (p : α × list α), f (p.fst :: p.snd)) ((nhds a).prod (nhds l)) b
theorem list.continuous_cons {α : Type u_1}  :
continuous (λ (x : α × list α), x.fst :: x.snd)
theorem list.tendsto_nhds {α : Type u_1} {β : Type u_2} {f : list α → β} {r : list α} (h_nil : (r list.nil)) (h_cons : ∀ (l : list α) (a : α), (nhds l) (r l)filter.tendsto (λ (p : α × list α), f (p.fst :: p.snd)) ((nhds a).prod (nhds l)) (r (a :: l))) (l : list α) :
(nhds l) (r l)
theorem list.continuous_at_length {α : Type u_1} (l : list α) :
theorem list.tendsto_insert_nth' {α : Type u_1} {a : α} {n : } {l : list α} :
filter.tendsto (λ (p : α × list α), p.snd) ((nhds a).prod (nhds l)) (nhds a l))
theorem list.tendsto_insert_nth {α : Type u_1} {β : Type u_2} {n : } {a : α} {l : list α} {f : β → α} {g : β → list α} {b : filter β} (hf : (nhds a)) (hg : (nhds l)) :
filter.tendsto (λ (b : β), (f b) (g b)) b (nhds a l))
theorem list.continuous_insert_nth {α : Type u_1} {n : } :
continuous (λ (p : α × list α), p.snd)
theorem list.tendsto_remove_nth {α : Type u_1} {n : } {l : list α} :
filter.tendsto (λ (l : list α), l.remove_nth n) (nhds l) (nhds (l.remove_nth n))
theorem list.continuous_remove_nth {α : Type u_1} {n : } :
continuous (λ (l : list α), l.remove_nth n)
theorem list.tendsto_sum {α : Type u_1} [add_monoid α] {l : list α} :
(nhds l.sum)
theorem list.tendsto_prod {α : Type u_1} [monoid α] {l : list α} :
(nhds l.prod)
theorem list.continuous_sum {α : Type u_1} [add_monoid α]  :
theorem list.continuous_prod {α : Type u_1} [monoid α]  :
@[protected, instance]
def vector.topological_space {α : Type u_1} (n : ) :
Equations
theorem vector.tendsto_cons {α : Type u_1} {n : } {a : α} {l : n} :
filter.tendsto (λ (p : α × n), p.fst ::ᵥ p.snd) ((nhds a).prod (nhds l)) (nhds (a ::ᵥ l))
theorem vector.tendsto_insert_nth {α : Type u_1} {n : } {i : fin (n + 1)} {a : α} {l : n} :
filter.tendsto (λ (p : α × n), p.snd) ((nhds a).prod (nhds l)) (nhds l))
theorem vector.continuous_insert_nth' {α : Type u_1} {n : } {i : fin (n + 1)} :
continuous (λ (p : α × n), p.snd)
theorem vector.continuous_insert_nth {α : Type u_1} {β : Type u_2} {n : } {i : fin (n + 1)} {f : β → α} {g : β → n} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), vector.insert_nth (f b) i (g b))
theorem vector.continuous_at_remove_nth {α : Type u_1} {n : } {i : fin (n + 1)} {l : (n + 1)} :
theorem vector.continuous_remove_nth {α : Type u_1} {n : } {i : fin (n + 1)} :