feat(analysis/topology): add continuity rules for list and vector insert/remove_nth

Author: johoelzl

analysis/topology/continuity.lean

@@ -761,24 +761,6 @@ lemma continuous_sum_rec {f : α → γ} {g : β → γ}
   (hf : continuous f) (hg : continuous g) : @continuous (α ⊕ β) γ _ _ (@sum.rec α β (λ_, γ) f g) :=
 continuous_inf_dom hf hg
 
-end sum
-
-section subtype
-variables [topological_space α] [topological_space β] [topological_space γ] {p : α → Prop}
-
-lemma embedding_graph {f : α → β} (hf : continuous f) : embedding (λx, (x, f x)) :=
-embedding_of_embedding_compose (continuous_id.prod_mk hf) continuous_fst embedding_id
-
-lemma embedding_subtype_val : embedding (@subtype.val α p) :=
-⟨assume a₁ a₂, subtype.eq, rfl⟩
-
-lemma continuous_subtype_val : continuous (@subtype.val α p) :=
-continuous_induced_dom
-
-lemma continuous_subtype_mk {f : β → α}
-  (hp : ∀x, p (f x)) (h : continuous f) : continuous (λx, (⟨f x, hp x⟩ : subtype p)) :=
-continuous_induced_rng h
-
 lemma embedding_inl : embedding (@sum.inl α β) :=
 ⟨λ _ _, sum.inl.inj_iff.mp,
   begin
@@ -815,6 +797,28 @@ lemma embedding_inr : embedding (@sum.inr α β) :=
     { rw induced_le_iff_le_coinduced, exact lattice.inf_le_right }
   end⟩
 
+end sum
+
+section subtype
+variables [topological_space α] [topological_space β] [topological_space γ] {p : α → Prop}
+
+lemma embedding_graph {f : α → β} (hf : continuous f) : embedding (λx, (x, f x)) :=
+embedding_of_embedding_compose (continuous_id.prod_mk hf) continuous_fst embedding_id
+
+lemma embedding_subtype_val : embedding (@subtype.val α p) :=
+⟨assume a₁ a₂, subtype.eq, rfl⟩
+
+lemma continuous_subtype_val : continuous (@subtype.val α p) :=
+continuous_induced_dom
+
+lemma continuous_subtype_mk {f : β → α}
+  (hp : ∀x, p (f x)) (h : continuous f) : continuous (λx, (⟨f x, hp x⟩ : subtype p)) :=
+continuous_induced_rng h
+
+lemma tendsto_subtype_val [topological_space α] {p : α → Prop} {a : subtype p} :
+  tendsto subtype.val (nhds a) (nhds a.val) :=
+continuous_iff_tendsto.1 continuous_subtype_val _
+
 lemma map_nhds_subtype_val_eq {a : α} (ha : p a) (h : {a | p a} ∈ (nhds a).sets) :
   map (@subtype.val α p) (nhds ⟨a, ha⟩) = nhds a :=
 map_nhds_induced_eq (by simp [subtype_val_image, h])
@@ -823,6 +827,10 @@ lemma nhds_subtype_eq_comap {a : α} {h : p a} :
   nhds (⟨a, h⟩ : subtype p) = comap subtype.val (nhds a) :=
 nhds_induced_eq_comap
 
+lemma tendsto_subtype_rng [topological_space α] {p : α → Prop} {b : filter β} {f : β → subtype p} :
+  ∀{a:subtype p}, tendsto f b (nhds a) ↔ tendsto (λx, subtype.val (f x)) b (nhds a.val)
+| ⟨a, ha⟩ := by rw [nhds_subtype_eq_comap, tendsto_comap_iff]
+
 lemma continuous_subtype_nhds_cover {ι : Sort*} {f : α → β} {c : ι → α → Prop}
   (c_cover : ∀x:α, ∃i, {x | c i x} ∈ (nhds x).sets)
   (f_cont  : ∀i, continuous (λ(x : subtype (c i)), f x.val)) :
@@ -1001,6 +1009,143 @@ end
 
 end pi
 
+namespace list
+variables [topological_space α] [topological_space β]
+
+lemma tendsto_cons' {a : α} {l : list α} :
+  tendsto (λp:α×list α, list.cons p.1 p.2) ((nhds a).prod (nhds l)) (nhds (a :: l)) :=
+by rw [nhds_cons, tendsto, map_prod]; exact le_refl _
+
+lemma tendsto_cons {f : α → β} {g : α → list β}
+  {a : _root_.filter α} {b : β} {l : list β} (hf : tendsto f a (nhds b)) (hg : tendsto g a (nhds l)):
+  tendsto (λa, list.cons (f a) (g a)) a (nhds (b :: l)) :=
+(tendsto.prod_mk hf hg).comp tendsto_cons'
+
+lemma tendsto_cons_iff [topological_space β]
+  {f : list α → β} {b : _root_.filter β} {a : α} {l : list α} :
+  tendsto f (nhds (a :: l)) b ↔ tendsto (λp:α×list α, f (p.1 :: p.2)) ((nhds a).prod (nhds l)) b :=
+have nhds (a :: l) = ((nhds a).prod (nhds l)).map (λp:α×list α, (p.1 :: p.2)),
+begin
+  simp only [nhds_cons, prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
+  simp [-filter.seq_eq_filter_seq, -filter.map_def, (∘)] with functor_norm,
+end,
+by rw [this, filter.tendsto_map'_iff]
+
+lemma tendsto_nhds [topological_space β]
+  {f : list α → β} {r : list α → _root_.filter β}
+  (h_nil : tendsto f (pure []) (r []))
+  (h_cons : ∀l a, tendsto f (nhds l) (r l) → tendsto (λp:α×list α, f (p.1 :: p.2)) ((nhds a).prod (nhds l)) (r (a::l))) :
+  ∀l, tendsto f (nhds l) (r l)
+| []     := by rwa [nhds_nil]
+| (a::l) := by rw [tendsto_cons_iff]; exact h_cons l a (tendsto_nhds l)
+
+lemma tendsto_length [topological_space α] :
+  ∀(l : list α), tendsto list.length (nhds l) (nhds l.length) :=
+begin
+  simp only [nhds_discrete],
+  refine tendsto_nhds _ _,
+  { exact tendsto_pure_pure _ _ },
+  { assume l a ih,
+    dsimp only [list.length],
+    refine tendsto.comp _ (tendsto_pure_pure (λx, x + 1) _),
+    refine tendsto.comp tendsto_snd ih }
+end
+
+lemma tendsto_insert_nth' {a : α} : ∀{n : ℕ} {l : list α},
+  tendsto (λp:α×list α, insert_nth n p.1 p.2) ((nhds a).prod (nhds l)) (nhds (insert_nth n a l))
+| 0     l  := tendsto_cons'
+| (n+1) [] :=
+  suffices tendsto (λa, []) (nhds a) (nhds ([] : list α)),
+    by simpa [nhds_nil, tendsto, map_prod, -filter.pure_def, (∘), insert_nth],
+  tendsto_const_nhds
+| (n+1) (a'::l) :=
+  have (nhds a).prod (nhds (a' :: l)) =
+    ((nhds a).prod ((nhds a').prod (nhds l))).map (λp:α×α×list α, (p.1, p.2.1 :: p.2.2)),
+  begin
+    simp only [nhds_cons, prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
+    simp [-filter.seq_eq_filter_seq, -filter.map_def, (∘)] with functor_norm
+  end,
+  begin
+    rw [this, tendsto_map'_iff],
+    exact tendsto_cons
+      (tendsto_snd.comp tendsto_fst)
+      ((tendsto.prod_mk tendsto_fst (tendsto_snd.comp tendsto_snd)).comp (@tendsto_insert_nth' n l))
+  end
+
+lemma tendsto_insert_nth {n : ℕ} {a : α} {l : list α} {f : β → α} {g : β → list α}
+  {b : _root_.filter β} (hf : tendsto f b (nhds a)) (hg : tendsto g b (nhds l)) :
+  tendsto (λb:β, insert_nth n (f b) (g b)) b (nhds (insert_nth n a l)) :=
+(tendsto.prod_mk hf hg).comp tendsto_insert_nth'
+
+lemma continuous_insert_nth {n : ℕ} : continuous (λp:α×list α, insert_nth n p.1 p.2) :=
+continuous_iff_tendsto.2 $ assume ⟨a, l⟩, by rw [nhds_prod_eq]; exact tendsto_insert_nth'
+
+lemma tendsto_remove_nth : ∀{n : ℕ} {l : list α},
+  tendsto (λl, remove_nth l n) (nhds l) (nhds (remove_nth l n))
+| _ []      := by rw [nhds_nil]; exact tendsto_pure_nhds _ _
+| 0 (a::l) := by rw [tendsto_cons_iff]; exact tendsto_snd
+| (n+1) (a::l) :=
+  begin
+    rw [tendsto_cons_iff],
+    dsimp [remove_nth],
+    exact tendsto_cons tendsto_fst (tendsto_snd.comp (@tendsto_remove_nth n l))
+  end
+
+lemma continuous_remove_nth {n : ℕ} : continuous (λl : list α, remove_nth l n) :=
+continuous_iff_tendsto.2 $ assume a, tendsto_remove_nth
+
+end list
+
+namespace vector
+open list filter
+
+instance (n : ℕ) [topological_space α] : topological_space (vector α n) :=
+by unfold vector; apply_instance
+
+lemma cons_val {n : ℕ} {a : α} : ∀{v : vector α n}, (a :: v).val = a :: v.val
+| ⟨l, hl⟩ := rfl
+
+lemma tendsto_cons [topological_space α] {n : ℕ} {a : α} {l : vector α n}:
+  tendsto (λp:α×vector α n, vector.cons p.1 p.2) ((nhds a).prod (nhds l)) (nhds (a :: l)) :=
+by
+  simp [tendsto_subtype_rng, cons_val];
+  exact tendsto_cons tendsto_fst (tendsto.comp tendsto_snd tendsto_subtype_val)
+
+lemma tendsto_insert_nth
+  [topological_space α] {n : ℕ} {i : fin (n+1)} {a:α} :
+  ∀{l:vector α n}, tendsto (λp:α×vector α n, insert_nth p.1 i p.2)
+    ((nhds a).prod (nhds l)) (nhds (insert_nth a i l))
+| ⟨l, hl⟩ :=
+begin
+  rw [insert_nth, tendsto_subtype_rng],
+  simp [insert_nth_val],
+  exact list.tendsto_insert_nth tendsto_fst (tendsto.comp tendsto_snd tendsto_subtype_val)
+end
+
+lemma continuous_insert_nth' [topological_space α] {n : ℕ} {i : fin (n+1)} :
+  continuous (λp:α×vector α n, insert_nth p.1 i p.2) :=
+continuous_iff_tendsto.2 $ assume ⟨a, l⟩, by rw [nhds_prod_eq]; exact tendsto_insert_nth
+
+lemma continuous_insert_nth [topological_space α] [topological_space β] {n : ℕ} {i : fin (n+1)}
+  {f : β → α} {g : β → vector α n} (hf : continuous f) (hg : continuous g) :
+  continuous (λb, insert_nth (f b) i (g b)) :=
+continuous.comp (continuous.prod_mk hf hg) continuous_insert_nth'
+
+lemma tendsto_remove_nth [topological_space α] {n : ℕ} {i : fin (n+1)} :
+  ∀{l:vector α (n+1)}, tendsto (remove_nth i) (nhds l) (nhds (remove_nth i l))
+| ⟨l, hl⟩ :=
+begin
+  rw [remove_nth, tendsto_subtype_rng],
+  simp [remove_nth_val],
+  exact tendsto_subtype_val.comp list.tendsto_remove_nth
+end
+
+lemma continuous_remove_nth [topological_space α] {n : ℕ} {i : fin (n+1)} :
+  continuous (remove_nth i : vector α (n+1) → vector α n) :=
+continuous_iff_tendsto.2 $ assume ⟨a, l⟩, tendsto_remove_nth
+
+end vector
+
 -- TODO: use embeddings from above!
 structure dense_embedding [topological_space α] [topological_space β] (e : α → β) : Prop :=
 (dense   : ∀x, x ∈ closure (range e))

analysis/topology/topological_space.lean

@@ -1060,6 +1060,13 @@ begin
       exact mem_traverse_sets _ _ (this.imp $ assume a s ⟨hs, ha⟩, mem_nhds_sets hs ha) } }
 end
 
+lemma nhds_nil [topological_space α] : nhds ([] : list α) = pure [] :=
+by rw [nhds_list, list.traverse_nil _]; apply_instance
+
+lemma nhds_cons [topological_space α] (a : α) (l : list α) :
+  nhds (a :: l) = list.cons <$> nhds a <*> nhds l  :=
+by rw [nhds_list, list.traverse_cons _, ← nhds_list]; apply_instance
+
 lemma quotient_dense_of_dense [setoid α] [topological_space α] {s : set α} (H : ∀ x, x ∈ closure s) :
   closure (quotient.mk '' s) = univ :=
 eq_univ_of_forall $ λ x, begin

analysis/topology/uniform_space.lean

@@ -1055,7 +1055,8 @@ instance : has_top (uniform_space α) :=
     rw [lift'_principal], {simp},
     exact monotone_comp_rel monotone_id monotone_id
   end,
-  is_open_uniformity := by simp [is_open_fold, subset_def, id_rel] {contextual := tt } } ⟩
+  is_open_uniformity :=
+    assume s, by simp [is_open_fold, subset_def, id_rel] {contextual := tt } } ⟩
 
 instance : complete_lattice (uniform_space α) :=
 { sup           := λa b, Sup {a, b},