Topology on lists and vectors #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
theorem
nhds_list
{α : Type u_1}
[topological_space α]
(as : list α) :
nhds as = traversable.traverse nhds as
@[simp]
theorem
filter.tendsto.cons
{β : Type u_2}
[topological_space β]
{α : Type u_1}
{f : α → β}
{g : α → list β}
{a : filter α}
{b : β}
{l : list β}
(hf : filter.tendsto f a (nhds b))
(hg : filter.tendsto g a (nhds l)) :
filter.tendsto (λ (a : α), f a :: g a) a (nhds (b :: l))
theorem
list.tendsto_nhds
{α : Type u_1}
[topological_space α]
{β : Type u_2}
{f : list α → β}
{r : list α → filter β}
(h_nil : filter.tendsto f (has_pure.pure list.nil) (r list.nil))
(h_cons : ∀ (l : list α) (a : α), filter.tendsto f (nhds l) (r l) → filter.tendsto (λ (p : α × list α), f (p.fst :: p.snd)) ((nhds a).prod (nhds l)) (r (a :: l)))
(l : list α) :
filter.tendsto f (nhds 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) ((nhds a).prod (nhds l)) (nhds (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 β}
(hf : filter.tendsto f b (nhds a))
(hg : filter.tendsto g b (nhds l)) :
filter.tendsto (λ (b : β), list.insert_nth n (f b) (g b)) b (nhds (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) (nhds l) (nhds (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 α} :
filter.tendsto list.sum (nhds l) (nhds l.sum)
theorem
list.tendsto_prod
{α : Type u_1}
[topological_space α]
[monoid α]
[has_continuous_mul α]
{l : list α} :
filter.tendsto list.prod (nhds l) (nhds l.prod)
theorem
list.continuous_sum
{α : Type u_1}
[topological_space α]
[add_monoid α]
[has_continuous_add α] :
theorem
list.continuous_prod
{α : Type u_1}
[topological_space α]
[monoid α]
[has_continuous_mul α] :
@[protected, instance]
def
vector.topological_space
{α : Type u_1}
[topological_space α]
(n : ℕ) :
topological_space (vector α n)
Equations
theorem
vector.tendsto_insert_nth
{α : Type u_1}
[topological_space α]
{n : ℕ}
{i : fin (n + 1)}
{a : α}
{l : vector α n} :
filter.tendsto (λ (p : α × vector α n), vector.insert_nth p.fst i p.snd) ((nhds a).prod (nhds l)) (nhds (vector.insert_nth a i l))
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}
(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}
[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)} :