rename towards -> tendsto

Author: johoelzl

algebra/lattice/filter.lean

@@ -975,46 +975,46 @@ le_antisymm
 
 end vmap
 
-/- towards -/
-def towards (f : α → β) (l₁ : filter α) (l₂ : filter β) := filter.map f l₁ ≤ l₂
+/- tendsto -/
+def tendsto (f : α → β) (l₁ : filter α) (l₂ : filter β) := filter.map f l₁ ≤ l₂
 
-lemma towards_cong {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
-  (h : towards f₁ l₁ l₂) (hl : {x | f₁ x = f₂ x} ∈ l₁.sets) : towards f₂ l₁ l₂ :=
-by rwa [towards, ←map_cong hl]
+lemma tendsto_cong {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
+  (h : tendsto f₁ l₁ l₂) (hl : {x | f₁ x = f₂ x} ∈ l₁.sets) : tendsto f₂ l₁ l₂ :=
+by rwa [tendsto, ←map_cong hl]
 
-lemma towards_id' {x y : filter α} : x ≤ y → towards id x y :=
-by simp [towards] { contextual := tt }
+lemma tendsto_id' {x y : filter α} : x ≤ y → tendsto id x y :=
+by simp [tendsto] { contextual := tt }
 
-lemma towards_id {x : filter α} : towards id x x := towards_id' $ le_refl x
+lemma tendsto_id {x : filter α} : tendsto id x x := tendsto_id' $ le_refl x
 
-lemma towards_compose {f : α → β} {g : β → γ} {x : filter α} {y : filter β} {z : filter γ}
-  (hf : towards f x y) (hg : towards g y z) : towards (g ∘ f) x z :=
+lemma tendsto_compose {f : α → β} {g : β → γ} {x : filter α} {y : filter β} {z : filter γ}
+  (hf : tendsto f x y) (hg : tendsto g y z) : tendsto (g ∘ f) x z :=
 calc map (g ∘ f) x = map g (map f x) : by rw [map_map]
   ... ≤ map g y : map_mono hf
   ... ≤ z : hg
 
-lemma towards_map {f : α → β} {x : filter α} : towards f x (map f x) := le_refl (map f x)
+lemma tendsto_map {f : α → β} {x : filter α} : tendsto f x (map f x) := le_refl (map f x)
 
-lemma towards_map' {f : β → γ} {g : α → β} {x : filter α} {y : filter γ}
-  (h : towards (f ∘ g) x y) : towards f (map g x) y :=
-by rwa [towards, map_map]
+lemma tendsto_map' {f : β → γ} {g : α → β} {x : filter α} {y : filter γ}
+  (h : tendsto (f ∘ g) x y) : tendsto f (map g x) y :=
+by rwa [tendsto, map_map]
 
-lemma towards_vmap {f : α → β} {x : filter β} : towards f (vmap f x) x :=
+lemma tendsto_vmap {f : α → β} {x : filter β} : tendsto f (vmap f x) x :=
 map_vmap_le
 
-lemma towards_vmap' {f : β → γ} {g : α → β} {x : filter α} {y : filter γ}
-  (h : towards (f ∘ g) x y) : towards g x (vmap f y) :=
+lemma tendsto_vmap' {f : β → γ} {g : α → β} {x : filter α} {y : filter γ}
+  (h : tendsto (f ∘ g) x y) : tendsto g x (vmap f y) :=
 le_vmap_iff_map_le.mpr $ by rwa [map_map]
 
-lemma towards_vmap'' {m : α → β} {f : filter α} {g : filter β} (s : set α)
+lemma tendsto_vmap'' {m : α → β} {f : filter α} {g : filter β} (s : set α)
   {i : γ → α} (hs : s ∈ f.sets) (hi : ∀a∈s, ∃c, i c = a)
-  (h : towards (m ∘ i) (vmap i f) g) : towards m f g :=
-have towards m (map i $ vmap i $ f) g,
-  by rwa [towards, ←map_compose] at h,
+  (h : tendsto (m ∘ i) (vmap i f) g) : tendsto m f g :=
+have tendsto m (map i $ vmap i $ f) g,
+  by rwa [tendsto, ←map_compose] at h,
 le_trans (map_mono $ le_map_vmap' hs hi) this
 
-lemma towards_inf {f : α → β} {x : filter α} {y₁ y₂ : filter β}
-  (h₁ : towards f x y₁) (h₂ : towards f x y₂) : towards f x (y₁ ⊓ y₂) :=
+lemma tendsto_inf {f : α → β} {x : filter α} {y₁ y₂ : filter β}
+  (h₁ : tendsto f x y₁) (h₂ : tendsto f x y₂) : tendsto f x (y₁ ⊓ y₂) :=
 le_inf h₁ h₂
 
 section lift
@@ -1382,16 +1382,16 @@ begin
     assume x, set.monotone_prod monotone_id monotone_const)
 end
 
-lemma towards_fst {f : filter α} {g : filter β} : towards prod.fst (filter.prod f g) f :=
+lemma tendsto_fst {f : filter α} {g : filter β} : tendsto prod.fst (filter.prod f g) f :=
 assume s hs, (filter.prod f g).upwards_sets (prod_mem_prod hs univ_mem_sets) $
   show set.prod s univ ⊆ preimage prod.fst s, by simp [set.prod, preimage] {contextual := tt}
 
-lemma towards_snd {f : filter α} {g : filter β} : towards prod.snd (filter.prod f g) g :=
+lemma tendsto_snd {f : filter α} {g : filter β} : tendsto prod.snd (filter.prod f g) g :=
 assume s hs, (filter.prod f g).upwards_sets (prod_mem_prod univ_mem_sets hs) $
   show set.prod univ s ⊆ preimage prod.snd s, by simp [set.prod, preimage] {contextual := tt}
 
-lemma towards_prod_mk {f : filter α} {g : filter β} {h : filter γ} {m₁ : α → β} {m₂ : α → γ}
-  (h₁ : towards m₁ f g) (h₂ : towards m₂ f h) : towards (λx, (m₁ x, m₂ x)) f (filter.prod g h) :=
+lemma tendsto_prod_mk {f : filter α} {g : filter β} {h : filter γ} {m₁ : α → β} {m₂ : α → γ}
+  (h₁ : tendsto m₁ f g) (h₂ : tendsto m₂ f h) : tendsto (λx, (m₁ x, m₂ x)) f (filter.prod g h) :=
 assume s hs,
 let ⟨s₁, hs₁, s₂, hs₂, h⟩ := mem_prod_iff.mp hs in
 f.upwards_sets (inter_mem_sets (h₁ hs₁) (h₂ hs₂)) $
@@ -1408,7 +1408,7 @@ le_antisymm
       calc set.prod (m₁ '' s₁) (m₂ '' s₂) = (λp:α₁×α₂, (m₁ p.1, m₂ p.2)) '' set.prod s₁ s₂ :
           set.prod_image_image_eq
         ... ⊆ _ : by rwa [image_subset_iff_subset_preimage])
-  (towards_prod_mk (towards_compose towards_fst (le_refl _)) (towards_compose towards_snd (le_refl _)))
+  (tendsto_prod_mk (tendsto_compose tendsto_fst (le_refl _)) (tendsto_compose tendsto_snd (le_refl _)))
 
 lemma prod_vmap_vmap_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
   {f₁ : filter α₁} {f₂ : filter α₂} {m₁ : β₁ → α₁} {m₂ : β₂ → α₂} :

topology/continuity.lean

@@ -45,22 +45,22 @@ lemma continuous_compose {f : α → β} {g : β → γ} (hf : continuous f) (hg
   continuous (g ∘ f) :=
 assume s h, hf _ (hg s h)
 
-lemma continuous_iff_towards {f : α → β} :
-  continuous f ↔ (∀x, towards f (nhds x) (nhds (f x))) :=
+lemma continuous_iff_tendsto {f : α → β} :
+  continuous f ↔ (∀x, tendsto f (nhds x) (nhds (f x))) :=
 ⟨assume hf : continuous f, assume x s,
   show s ∈ (nhds (f x)).sets → s ∈ (map f (nhds x)).sets,
     by simp [nhds_sets];
       exact assume ⟨t, t_open, t_subset, fx_in_t⟩,
         ⟨preimage f t, hf t t_open, fx_in_t, preimage_mono t_subset⟩,
-  assume hf : ∀x, towards f (nhds x) (nhds (f x)),
+  assume hf : ∀x, tendsto f (nhds x) (nhds (f x)),
   assume s, assume hs : is_open s,
   have ∀a, f a ∈ s → s ∈ (nhds (f a)).sets,
     by simp [nhds_sets]; exact assume a ha, ⟨s, hs, subset.refl s, ha⟩,
   show is_open (preimage f s),
     by simp [is_open_iff_nhds]; exact assume a ha, hf a (this a ha)⟩
 
 lemma continuous_const [topological_space α] [topological_space β] {b : β} : continuous (λa:α, b) :=
-continuous_iff_towards.mpr $ assume a, towards_const_nhds
+continuous_iff_tendsto.mpr $ assume a, tendsto_const_nhds
 
 lemma continuous_iff_is_closed {f : α → β} :
   continuous f ↔ (∀s, is_closed s → is_closed (preimage f s)) :=
@@ -75,7 +75,7 @@ have ∀ (a : α), nhds a ⊓ principal s ≠ ⊥ → nhds (f a) ⊓ principal (
     by rwa[map_eq_bot_iff],
   have h₂ : map f (nhds a ⊓ principal s) ≤ nhds (f a) ⊓ principal (f '' s),
     from le_inf
-      (le_trans (map_mono inf_le_left) $ by rw [continuous_iff_towards] at h; exact h a)
+      (le_trans (map_mono inf_le_left) $ by rw [continuous_iff_tendsto] at h; exact h a)
       (le_trans (map_mono inf_le_right) $ by simp; exact subset.refl _),
   neq_bot_of_le_neq_bot h₁ h₂,
 by simp [image_subset_iff_subset_preimage, closure_eq_nhds]; assumption
@@ -292,7 +292,7 @@ le_antisymm
 lemma map_nhds_induced_eq {a : α} (h : image f univ ∈ (nhds (f a)).sets) :
   map f (@nhds α (induced f t) a) = nhds (f a) :=
 le_antisymm
-  ((@continuous_iff_towards α β (induced f t) _ _).mp continuous_induced_dom a)
+  ((@continuous_iff_tendsto α β (induced f t) _ _).mp continuous_induced_dom a)
   (assume s, assume hs : preimage f s ∈ (@nhds α (induced f t) a).sets,
     let ⟨t', t_subset, is_open_t, a_in_t⟩ := mem_nhds_sets_iff.mp h in
     let ⟨s', s'_subset, ⟨s'', is_open_s'', s'_eq⟩, a_in_s'⟩ := (@mem_nhds_sets_iff _ (induced f t) _ _).mp hs in
@@ -426,13 +426,13 @@ end sum
 section subtype
 variables [topological_space α] [topological_space β] [topological_space γ] {p : α → Prop}
 
-lemma towards_nhds_iff_of_embedding {f : α → β} {g : β → γ} {a : filter α} {b : β} (hg : embedding g) :
-  towards f a (nhds b) ↔ towards (g ∘ f) a (nhds (g b)) :=
-by rw [towards, towards, hg.right, nhds_induced_eq_vmap, le_vmap_iff_map_le, map_map]
+lemma tendsto_nhds_iff_of_embedding {f : α → β} {g : β → γ} {a : filter α} {b : β} (hg : embedding g) :
+  tendsto f a (nhds b) ↔ tendsto (g ∘ f) a (nhds (g b)) :=
+by rw [tendsto, tendsto, hg.right, nhds_induced_eq_vmap, le_vmap_iff_map_le, map_map]
 
 lemma continuous_iff_of_embedding {f : α → β} {g : β → γ} (hg : embedding g) :
   continuous f ↔ continuous (g ∘ f) :=
-by simp [continuous_iff_towards, @towards_nhds_iff_of_embedding α β γ _ _ _ f g _ _ hg]
+by simp [continuous_iff_tendsto, @tendsto_nhds_iff_of_embedding α β γ _ _ _ f g _ _ hg]
 
 lemma embedding_graph {f : α → β} (hf : continuous f) : embedding (λx, (x, f x)) :=
 embedding_of_embedding_compose (continuous_prod_mk continuous_id hf) continuous_fst embedding_id
@@ -459,13 +459,13 @@ lemma continuous_subtype_nhds_cover {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)) :
   continuous f :=
-continuous_iff_towards.mpr $ assume x,
+continuous_iff_tendsto.mpr $ assume x,
   let ⟨i, (c_sets : {x | c i x} ∈ (nhds x).sets)⟩ := c_cover x in
   let x' : subtype (c i) := ⟨x, mem_of_nhds c_sets⟩ in
   calc map f (nhds x) = map f (map subtype.val (nhds x')) :
       congr_arg (map f) (map_nhds_subtype_val_eq _ $ c_sets).symm
     ... = map (λx:subtype (c i), f x.val) (nhds x') : rfl
-    ... ≤ nhds (f x) : continuous_iff_towards.mp (f_cont i) x'
+    ... ≤ nhds (f x) : continuous_iff_tendsto.mp (f_cont i) x'
 
 lemma continuous_subtype_is_closed_cover {f : α → β} (c : γ → α → Prop)
   (h_lf : locally_finite (λi, {x | c i x}))
@@ -536,11 +536,11 @@ variables {e : α → β} (de : dense_embedding e)
 protected lemma embedding (de : dense_embedding e) : embedding e :=
 ⟨de.inj, eq_of_nhds_eq_nhds begin intro a, rw [← de.induced a, nhds_induced_eq_vmap] end⟩
 
-protected lemma towards (de : dense_embedding e) {a : α} : towards e (nhds a) (nhds (e a)) :=
-by rw [←de.induced a]; exact towards_vmap
+protected lemma tendsto (de : dense_embedding e) {a : α} : tendsto e (nhds a) (nhds (e a)) :=
+by rw [←de.induced a]; exact tendsto_vmap
 
 protected lemma continuous (de : dense_embedding e) {a : α} : continuous e :=
-by rw [continuous_iff_towards]; exact assume a, de.towards
+by rw [continuous_iff_tendsto]; exact assume a, de.tendsto
 
 lemma inj_iff (de : dense_embedding e) {x y} : e x = e y ↔ x = y :=
 ⟨de.inj _ _, assume h, h ▸ rfl⟩
@@ -574,13 +574,13 @@ lemma ext_e_eq {a : α} {f : α → γ} (de : dense_embedding e)
   (hf : map f (nhds a) ≤ nhds (f a)) : de.ext f (e a) = f a :=
 de.ext_eq begin rw de.induced; exact hf end
 
-lemma towards_ext {b : β} {f : α → γ} (de : dense_embedding e)
-  (hf : {b | ∃c, towards f (vmap e $ nhds b) (nhds c)} ∈ (nhds b).sets) :
-  towards (de.ext f) (nhds b) (nhds (de.ext f b)) :=
-let φ := {b | towards f (vmap e $ nhds b) (nhds $ de.ext f b)} in
+lemma tendsto_ext {b : β} {f : α → γ} (de : dense_embedding e)
+  (hf : {b | ∃c, tendsto f (vmap e $ nhds b) (nhds c)} ∈ (nhds b).sets) :
+  tendsto (de.ext f) (nhds b) (nhds (de.ext f b)) :=
+let φ := {b | tendsto f (vmap e $ nhds b) (nhds $ de.ext f b)} in
 have hφ : φ ∈ (nhds b).sets,
   from (nhds b).upwards_sets hf $ assume b ⟨c, hc⟩,
-    show towards f (vmap e (nhds b)) (nhds (de.ext f b)), from (de.ext_eq hc).symm ▸ hc,
+    show tendsto f (vmap e (nhds b)) (nhds (de.ext f b)), from (de.ext_eq hc).symm ▸ hc,
 assume s hs,
 let ⟨s'', hs''₁, hs''₂, hs''₃⟩ := nhds_is_closed hs in
 let ⟨s', hs'₁, (hs'₂ : preimage e s' ⊆ preimage f s'')⟩ := mem_of_nhds hφ hs''₁ in
@@ -612,8 +612,8 @@ have h₂ : t ⊆ preimage (de.ext f) (closure (f '' preimage e t)), from
     ... ⊆ preimage (de.ext f) s : preimage_mono hs''₂)
 
 lemma continuous_ext {f : α → γ} (de : dense_embedding e)
-  (hf : ∀b, ∃c, towards f (vmap e (nhds b)) (nhds c)) : continuous (de.ext f) :=
-continuous_iff_towards.mpr $ assume b, de.towards_ext $ univ_mem_sets' hf
+  (hf : ∀b, ∃c, tendsto f (vmap e (nhds b)) (nhds c)) : continuous (de.ext f) :=
+continuous_iff_tendsto.mpr $ assume b, de.tendsto_ext $ univ_mem_sets' hf
 
 end dense_embedding