feat(topology/basic): Lim_spec etc. cleanup (#4545)

Fixes #4543
See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/More.20point.20set.20topology.20questions/near/212757136)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: adamtopaz

src/order/filter/ultrafilter.lean

@@ -143,7 +143,7 @@ begin
 end
 
 lemma exists_ultrafilter_of_finite_inter_nonempty (S : set (set α)) (cond : ∀ T : finset (set α),
-  (↑T : set (set α)) ⊆ S → (⋂₀ (↑T : set (set α))).nonempty) : 
+  (↑T : set (set α)) ⊆ S → (⋂₀ (↑T : set (set α))).nonempty) :
   ∃ F : filter α, S ⊆ F.sets ∧ is_ultrafilter F :=
 begin
   suffices : ∃ F : filter α, ne_bot F ∧ S ⊆ F.sets,
@@ -247,6 +247,8 @@ instance ultrafilter.monad : monad ultrafilter := { map := @ultrafilter.map }
 
 instance ultrafilter.inhabited [inhabited α] : inhabited (ultrafilter α) := ⟨pure (default _)⟩
 
+instance {F : ultrafilter α} : ne_bot F.1 := F.2.1
+
 /-- The ultra-filter extending the cofinite filter. -/
 noncomputable def hyperfilter : filter α := ultrafilter_of cofinite
 

src/topology/basic.lean

@@ -823,16 +823,16 @@ Lim (f.map g)
 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) :=
+lemma le_nhds_Lim {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)) :
+lemma tendsto_nhds_lim {f : filter β} {g : β → α} (h : ∃ a, tendsto g f (𝓝 a)) :
   tendsto g f (𝓝 $ @lim _ _ _ (nonempty_of_exists h) f g) :=
-Lim_spec h
+le_nhds_Lim h
 
 end lim
 

src/topology/extend_from_subset.lean

@@ -39,13 +39,13 @@ def extend_from (A : set X) (f : X → Y) : X → Y :=
 then `f` tends to `extend_from A f x` as `x` tends to `x₀`. -/
 lemma tendsto_extend_from {A : set X} {f : X → Y} {x : X}
   (h : ∃ y, tendsto f (nhds_within x A) (𝓝 y)) : tendsto f (nhds_within x A) (𝓝 $ extend_from A f x) :=
-lim_spec h
+tendsto_nhds_lim h
 
 lemma extend_from_eq [t2_space Y] {A : set X} {f : X → Y} {x : X} {y : Y} (hx : x ∈ closure A)
   (hf : tendsto f (nhds_within x A) (𝓝 y)) : extend_from A f x = y :=
 begin
   haveI := mem_closure_iff_nhds_within_ne_bot.mp hx,
-  exact tendsto_nhds_unique (lim_spec ⟨y, hf⟩) hf,
+  exact tendsto_nhds_unique (tendsto_nhds_lim ⟨y, hf⟩) hf,
 end
 
 lemma extend_from_extends [t2_space Y] {f : X → Y} {A : set X} (hf : continuous_on f A) :

src/topology/separation.lean

@@ -188,13 +188,23 @@ are useful without a `nonempty α` instance.
 
 lemma Lim_eq {a : α} [ne_bot f] (h : f ≤ 𝓝 a) :
   @Lim _ _ ⟨a⟩ f = a :=
-tendsto_nhds_unique (Lim_spec ⟨a, h⟩) h
+tendsto_nhds_unique (le_nhds_Lim ⟨a, h⟩) h
 
-lemma filter.tendsto.lim_eq {a : α} {f : filter β} {g : β → α} (h : tendsto g f (𝓝 a))
-  [ne_bot f] :
+lemma Lim_eq_iff [ne_bot f] (h : ∃ (a : α), f ≤ nhds a) {a} : @Lim _ _ ⟨a⟩ f = a ↔ f ≤ 𝓝 a :=
+⟨λ c, c ▸ le_nhds_Lim h, Lim_eq⟩
+
+lemma is_ultrafilter.Lim_eq_iff_le_nhds [compact_space α] (x : α) (F : ultrafilter α) :
+  @Lim _ _ ⟨x⟩ F.1 = x ↔ F.1 ≤ 𝓝 x :=
+⟨λ h, h ▸ is_ultrafilter.le_nhds_Lim _, Lim_eq⟩
+
+lemma filter.tendsto.lim_eq {a : α} {f : filter β} [ne_bot f] {g : β → α} (h : tendsto g f (𝓝 a)) :
   @lim _ _ _ ⟨a⟩ f g = a :=
 Lim_eq h
 
+lemma filter.lim_eq_iff {f : filter β} [ne_bot f] {g : β → α} (h : ∃ a, tendsto g f (𝓝 a)) {a} :
+  @lim _ _ _ ⟨a⟩ f g = a ↔ tendsto g f (𝓝 a) :=
+⟨λ c, c ▸ tendsto_nhds_lim h, filter.tendsto.lim_eq⟩
+
 lemma continuous.lim_eq [topological_space β] {f : β → α} (h : continuous f) (a : β) :
   @lim _ _ _ ⟨f a⟩ (𝓝 a) f = f a :=
 (h.tendsto a).lim_eq

src/topology/subset_properties.lean

@@ -593,6 +593,13 @@ begin
   rwa [← mem_interior_iff_mem_nhds, hU.interior_eq]
 end
 
+lemma is_ultrafilter.le_nhds_Lim [compact_space α] (F : ultrafilter α) :
+  F.1 ≤ nhds (@Lim _ _ F.1.nonempty_of_ne_bot F.1) :=
+begin
+  rcases compact_iff_ultrafilter_le_nhds.mp compact_univ F.1 F.2 (by simp) with ⟨x, -, h⟩,
+  exact le_nhds_Lim ⟨x,h⟩,
+end
+
 end compact
 
 section clopen

src/topology/uniform_space/cauchy.lean

@@ -266,7 +266,7 @@ h₁ _ h₃ $ le_principal_iff.2 $ mem_map_sets_iff.2 ⟨univ, univ_mem_sets,
 
 theorem cauchy.le_nhds_Lim [complete_space α] [nonempty α] {f : filter α} (hf : cauchy f) :
   f ≤ 𝓝 (Lim f) :=
-Lim_spec (complete_space.complete hf)
+le_nhds_Lim (complete_space.complete hf)
 
 theorem cauchy_seq.tendsto_lim [semilattice_sup β] [complete_space α] [nonempty α] {u : β → α}
   (h : cauchy_seq u) :

src/topology/uniform_space/uniform_embedding.lean

@@ -385,7 +385,7 @@ 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 (uniformly_extend_exists h_e h_dense h_f _) }
+    exact tendsto_nhds_lim (uniformly_extend_exists h_e h_dense h_f _) }
 end
 
 lemma uniform_continuous_uniformly_extend [cγ : complete_space γ] : uniform_continuous ψ :=