refactor(topology): rename lim to Lim (#2977)

Also introduce `lim (f : filter α) (g : α → β)`.

src/dynamics/circle/rotation_number/translation_number.lean

@@ -375,7 +375,7 @@ def transnum_aux_seq (n : ℕ) : ℝ := (f^(2^n)) 0 / 2^n
 an auxiliary sequence `\frac{f^{2^n}(0)}{2^n}` to define `τ(f)` because some proofs are simpler
 this way. -/
 def translation_number : ℝ :=
-lim ((at_top : filter ℕ).map f.transnum_aux_seq)
+lim at_top f.transnum_aux_seq
 
 -- TODO: choose two different symbols for `circle_deg1_lift.translation_number` and the future
 -- `circle_mono_homeo.rotation_number`, then make them `localized notation`s
@@ -386,7 +386,7 @@ lemma transnum_aux_seq_def : f.transnum_aux_seq = λ n : ℕ, (f^(2^n)) 0 / 2^n
 lemma translation_number_eq_of_tendsto_aux {τ' : ℝ}
   (h : tendsto f.transnum_aux_seq at_top (𝓝 τ')) :
   τ f = τ' :=
-lim_eq (map_ne_bot at_top_ne_bot) h
+h.lim_eq at_top_ne_bot
 
 lemma translation_number_eq_of_tendsto₀ {τ' : ℝ}
   (h : tendsto (λ n:ℕ, f^[n] 0 / n) at_top (𝓝 τ')) :
@@ -415,8 +415,7 @@ begin
 end
 
 lemma tendsto_translation_number_aux : tendsto f.transnum_aux_seq at_top (𝓝 $ τ f) :=
-le_nhds_lim_of_cauchy $ cauchy_seq_of_le_geometric_two 1
-  (λ n, le_of_lt $ f.transnum_aux_seq_dist_lt n)
+(cauchy_seq_of_le_geometric_two 1 (λ n, le_of_lt $ f.transnum_aux_seq_dist_lt n)).tendsto_lim
 
 lemma dist_map_zero_translation_number_le : dist (f 0) (τ f) ≤ 1 :=
 f.transnum_aux_seq_zero ▸ dist_le_of_le_geometric_two_of_tendsto₀ 1

src/topology/basic.lean

@@ -596,15 +596,32 @@ begin
 end
 
 section lim
-variables [nonempty α]
 
-/-- If `f` is a filter, then `lim f` is a limit of the filter, if it exists. -/
-noncomputable def lim (f : filter α) : α := epsilon $ λa, f ≤ 𝓝 a
+/-- If `f` is a filter, then `Lim f` is a limit of the filter, if it exists. -/
+noncomputable def Lim [nonempty α] (f : filter α) : α := epsilon $ λa, f ≤ 𝓝 a
+
+/-- If `f` is a filter in `β` and `g : β → α` is a function, then `lim f` is a limit of `g` at `f`,
+if it exists. -/
+noncomputable def lim [nonempty α] (f : filter β) (g : β → α) : α :=
+Lim (f.map g)
+
+/-- If a filter `f` is majorated by some `𝓝 a`, then it is majorated by `𝓝 (Lim f)`. We formulate
+this lemma with a `[nonempty α]` argument of `Lim` derived from `h` to make it useful for types
+without a `[nonempty α]` instance. Because of the built-in proof irrelevance, Lean will unify
+this instance with any other instance. -/
+lemma Lim_spec {f : filter α} (h : ∃a, f ≤ 𝓝 a) : f ≤ 𝓝 (@Lim _ _ (nonempty_of_exists h) f) :=
+epsilon_spec h
+
+/-- If `g` tends to some `𝓝 a` along `f`, then it tends to `𝓝 (lim f g)`. We formulate
+this lemma with a `[nonempty α]` argument of `lim` derived from `h` to make it useful for types
+without a `[nonempty α]` instance. Because of the built-in proof irrelevance, Lean will unify
+this instance with any other instance. -/
+lemma lim_spec {f : filter β} {g : β → α} (h : ∃ a, tendsto g f (𝓝 a)) :
+  tendsto g f (𝓝 $ @lim _ _ _ (nonempty_of_exists h) f g) :=
+Lim_spec h
 
-lemma lim_spec {f : filter α} (h : ∃a, f ≤ 𝓝 a) : f ≤ 𝓝 (lim f) := epsilon_spec h
 end lim
 
-
 /- locally finite family [General Topology (Bourbaki, 1995)] -/
 section locally_finite
 

src/topology/dense_embedding.lean

@@ -159,11 +159,11 @@ variables [topological_space γ]
   continuous extension, then `g` is the unique such extension. In general,
   `g` might not be continuous or even extend `f`. -/
 def extend (di : dense_inducing i) (f : α → γ) (b : β) : γ :=
-@lim _ _ ⟨f (dense_range.inhabited di.dense b).default⟩ (map f (comap i (𝓝 b)))
+@@lim _ ⟨f (di.dense.inhabited b).default⟩ (comap i (𝓝 b)) f
 
-lemma extend_eq [t2_space γ] {b : β} {c : γ} {f : α → γ} (hf : map f (comap i (𝓝 b)) ≤ 𝓝 c) :
+lemma extend_eq [t2_space γ] {b : β} {c : γ} {f : α → γ} (hf : tendsto f (comap i (𝓝 b)) (𝓝 c)) :
   di.extend f b = c :=
-@lim_eq _ _ (id _) _ _ _ (by simp; exact comap_nhds_ne_bot di) hf
+hf.lim_eq di.comap_nhds_ne_bot
 
 lemma extend_e_eq [t2_space γ] {f : α → γ} (a : α) (hf : continuous_at f a) :
   di.extend f (i a) = f a :=

src/topology/separation.lean

@@ -133,17 +133,42 @@ lemma tendsto_nhds_unique [t2_space α] {f : β → α} {l : filter β} {a b : 
 eq_of_nhds_ne_bot $ ne_bot_of_le_ne_bot (map_ne_bot hl) $ le_inf ha hb
 
 section lim
-variables [nonempty α] [t2_space α] {f : filter α}
+variables [t2_space α] {f : filter α}
 
-lemma lim_eq {a : α} (hf : f ≠ ⊥) (h : f ≤ 𝓝 a) : lim f = a :=
-eq_of_nhds_ne_bot $ ne_bot_of_le_ne_bot hf $ le_inf (lim_spec ⟨_, h⟩) h
+/-!
+### Properties of `Lim` and `lim`
 
-@[simp] lemma lim_nhds_eq {a : α} : lim (𝓝 a) = a :=
-lim_eq nhds_ne_bot (le_refl _)
+In this section we use explicit `nonempty α` instances for `Lim` and `lim`. This way the lemmas
+are useful without a `nonempty α` instance.
+-/
+
+lemma Lim_eq {a : α} (hf : f ≠ ⊥) (h : f ≤ 𝓝 a) :
+  @Lim _ _ ⟨a⟩ f = a :=
+tendsto_nhds_unique hf (Lim_spec ⟨a, h⟩) h
+
+lemma filter.tendsto.lim_eq {a : α} {f : filter β} {g : β → α} (h : tendsto g f (𝓝 a))
+  (hf : f ≠ ⊥) :
+  @lim _ _ _ ⟨a⟩ f g = a :=
+Lim_eq (map_ne_bot hf) h
+
+lemma continuous.lim_eq [topological_space β] {f : β → α} (h : continuous f) (a : β) :
+  @lim _ _ _ ⟨f a⟩ (𝓝 a) f = f a :=
+(h.tendsto a).lim_eq nhds_ne_bot
+
+@[simp] lemma Lim_nhds (a : α) : @Lim _ _ ⟨a⟩ (𝓝 a) = a :=
+Lim_eq nhds_ne_bot (le_refl _)
+
+@[simp] lemma lim_nhds_id (a : α) : @lim _ _ _ ⟨a⟩ (𝓝 a) id = a :=
+Lim_nhds a
+
+@[simp] lemma Lim_nhds_within {a : α} {s : set α} (h : a ∈ closure s) :
+  @Lim _ _ ⟨a⟩ (nhds_within a s) = a :=
+Lim_eq begin rw [closure_eq_nhds] at h, exact h end inf_le_left
+
+@[simp] lemma lim_nhds_within_id {a : α} {s : set α} (h : a ∈ closure s) :
+  @lim _ _ _ ⟨a⟩ (nhds_within a s) id = a :=
+Lim_nhds_within h
 
-@[simp] lemma lim_nhds_eq_of_closure {a : α} {s : set α} (h : a ∈ closure s) :
-  lim (𝓝 a ⊓ principal s) = a :=
-lim_eq begin rw [closure_eq_nhds] at h, exact h end inf_le_left
 end lim
 
 @[priority 100] -- see Note [lower instance priority]

src/topology/uniform_space/cauchy.lean

@@ -246,9 +246,14 @@ lemma cauchy_seq_tendsto_of_is_complete [semilattice_sup β] {K : set α} (h₁
 h₁ _ h₃ $ le_principal_iff.2 $ mem_map_sets_iff.2 ⟨univ, univ_mem_sets,
   by { simp only [image_univ], rintros _ ⟨n, rfl⟩, exact h₂ n }⟩
 
-theorem le_nhds_lim_of_cauchy {α} [uniform_space α] [complete_space α]
-  [nonempty α] {f : filter α} (hf : cauchy f) : f ≤ 𝓝 (lim f) :=
-lim_spec (complete_space.complete hf)
+theorem cauchy.le_nhds_Lim [complete_space α] [nonempty α] {f : filter α} (hf : cauchy f) :
+  f ≤ 𝓝 (Lim f) :=
+Lim_spec (complete_space.complete hf)
+
+theorem cauchy_seq.tendsto_lim [semilattice_sup β] [complete_space α] [nonempty α] {u : β → α}
+  (h : cauchy_seq u) :
+  tendsto u at_top (𝓝 $ lim at_top u) :=
+h.le_nhds_Lim
 
 lemma is_complete_of_is_closed [complete_space α] {s : set α}
   (h : is_closed s) : is_complete s :=

src/topology/uniform_space/completion.lean

@@ -251,30 +251,30 @@ end
 
 theorem Cauchy_eq
   {α : Type*} [inhabited α] [uniform_space α] [complete_space α] [separated α] {f g : Cauchy α} :
-  lim f.1 = lim g.1 ↔ (f, g) ∈ separation_rel (Cauchy α) :=
+  Lim f.1 = Lim g.1 ↔ (f, g) ∈ separation_rel (Cauchy α) :=
 begin
   split,
   { intros e s hs,
     rcases Cauchy.mem_uniformity'.1 hs with ⟨t, tu, ts⟩,
     apply ts,
     rcases comp_mem_uniformity_sets tu with ⟨d, du, dt⟩,
     refine mem_prod_iff.2
-      ⟨_, le_nhds_lim_of_cauchy f.2 (mem_nhds_right (lim f.1) du),
-       _, le_nhds_lim_of_cauchy g.2 (mem_nhds_left (lim g.1) du), λ x h, _⟩,
+      ⟨_, f.2.le_nhds_Lim (mem_nhds_right (Lim f.1) du),
+       _, g.2.le_nhds_Lim (mem_nhds_left (Lim g.1) du), λ x h, _⟩,
     cases x with a b, cases h with h₁ h₂,
     rw ← e at h₂,
     exact dt ⟨_, h₁, h₂⟩ },
   { intros H,
     refine separated_def.1 (by apply_instance) _ _ (λ t tu, _),
     rcases mem_uniformity_is_closed tu with ⟨d, du, dc, dt⟩,
-    refine H {p | (lim p.1.1, lim p.2.1) ∈ t}
+    refine H {p | (Lim p.1.1, Lim p.2.1) ∈ t}
       (Cauchy.mem_uniformity'.2 ⟨d, du, λ f g h, _⟩),
     rcases mem_prod_iff.1 h with ⟨x, xf, y, yg, h⟩,
-    have limc : ∀ (f : Cauchy α) (x ∈ f.1), lim f.1 ∈ closure x,
+    have limc : ∀ (f : Cauchy α) (x ∈ f.1), Lim f.1 ∈ closure x,
     { intros f x xf,
       rw closure_eq_nhds,
       exact ne_bot_of_le_ne_bot f.2.1
-        (le_inf (le_nhds_lim_of_cauchy f.2) (le_principal_iff.2 xf)) },
+        (le_inf f.2.le_nhds_Lim (le_principal_iff.2 xf)) },
     have := (closure_subset_iff_subset_of_is_closed dc).2 h,
     rw closure_prod_eq at this,
     refine dt (this ⟨_, _⟩); dsimp; apply limc; assumption }

src/topology/uniform_space/uniform_embedding.lean

@@ -378,9 +378,10 @@ begin
     rw [uniformly_extend_of_ind _ _ h_f, ← de.nhds_eq_comap],
     exact h_f.continuous.tendsto _ },
   { simp only [dense_inducing.extend, dif_neg ha],
-    exact (@lim_spec _ _ (id _) _ $ uniformly_extend_exists h_e h_dense h_f _) }
+    exact lim_spec (uniformly_extend_exists h_e h_dense h_f _) }
 end
 
+
 lemma uniform_continuous_uniformly_extend [cγ : complete_space γ] : uniform_continuous ψ :=
 assume d hd,
 let ⟨s, hs, hs_comp⟩ := (mem_lift'_sets $