feat(topology/uniform_space/cauchy): add cauchy_seq.comp_injective (#…

…11986)

API changes:

- add `filter.at_top_le_cofinite`;
- add `function.injective.nat_tendsto_at_top`;
- add `cauchy_seq.comp_injective`, `function.bijective.cauchy_seq_comp_iff`.



Co-authored-by: Mark Andrew Gerads <MarkAndrewGerads.Nazgand@Gmail.Com>

src/order/filter/cofinite.lean

@@ -20,7 +20,7 @@ and prove its basic properties. In particular, we prove that for `ℕ` it is equ
 Define filters for other cardinalities of the complement.
 -/
 
-open set
+open set function
 open_locale classical
 
 variables {α : Type*}
@@ -80,7 +80,7 @@ begin
   split,
   { rintro ⟨t, htf, hsub⟩,
     exact (finite.pi htf).subset hsub },
-  { exact λ hS, ⟨λ i, function.eval i '' S, λ i, hS.image _, subset_pi_eval_image _ _⟩ }
+  { exact λ hS, ⟨λ i, eval i '' S, λ i, hS.image _, subset_pi_eval_image _ _⟩ }
 end
 
 end filter
@@ -103,23 +103,23 @@ frequently_cofinite_iff_infinite.symm
 lemma filter.eventually_cofinite_ne (x : α) : ∀ᶠ a in cofinite, a ≠ x :=
 (set.finite_singleton x).eventually_cofinite_nmem
 
+/-- If `α` is a sup-semilattice with no maximal element, then `at_top ≤ cofinite`. -/
+lemma at_top_le_cofinite [semilattice_sup α] [no_max_order α] : (at_top : filter α) ≤ cofinite :=
+begin
+  refine compl_surjective.forall.2 (λ s hs, _),
+  rcases eq_empty_or_nonempty s with rfl|hne, { simp only [compl_empty, univ_mem] },
+  rw [mem_cofinite, compl_compl] at hs, lift s to finset α using hs,
+  rcases exists_gt (s.sup' hne id) with ⟨y, hy⟩,
+  filter_upwards [mem_at_top y] with x hx hxs,
+  exact (finset.le_sup' id hxs).not_lt (hy.trans_le hx)
+end
+
 /-- For natural numbers the filters `cofinite` and `at_top` coincide. -/
 lemma nat.cofinite_eq_at_top : @cofinite ℕ = at_top :=
 begin
-  ext s,
-  simp only [mem_cofinite, mem_at_top_sets],
-  split,
-  { assume hs,
-    use (hs.to_finset.sup id) + 1,
-    assume b hb,
-    by_contradiction hbs,
-    have := hs.to_finset.subset_range_sup_succ (hs.mem_to_finset.2 hbs),
-    exact not_lt_of_le hb (finset.mem_range.1 this) },
-  { rintros ⟨N, hN⟩,
-    apply (finite_lt_nat N).subset,
-    assume n hn,
-    change n < N,
-    exact lt_of_not_ge (λ hn', hn $ hN n hn') }
+  refine le_antisymm _ at_top_le_cofinite,
+  refine at_top_basis.ge_iff.2 (λ N hN, _),
+  simpa only [mem_cofinite, compl_Ici] using finite_lt_nat N
 end
 
 lemma nat.frequently_at_top_iff_infinite {p : ℕ → Prop} :
@@ -162,6 +162,12 @@ lemma filter.tendsto.exists_forall_ge {α β : Type*} [nonempty α] [linear_orde
 @filter.tendsto.exists_forall_le _ (order_dual β) _ _ _ hf
 
 /-- For an injective function `f`, inverse images of finite sets are finite. -/
-lemma function.injective.tendsto_cofinite {α β : Type*} {f : α → β} (hf : function.injective f) :
+lemma function.injective.tendsto_cofinite {α β : Type*} {f : α → β} (hf : injective f) :
   tendsto f cofinite cofinite :=
 λ s h, h.preimage (hf.inj_on _)
+
+/-- An injective sequence `f : ℕ → ℕ` tends to infinity at infinity. -/
+lemma function.injective.nat_tendsto_at_top {f : ℕ → ℕ} (hf : injective f) :
+  tendsto f at_top at_top :=
+nat.cofinite_eq_at_top ▸ hf.tendsto_cofinite
+

src/topology/uniform_space/cauchy.lean

@@ -10,7 +10,7 @@ import topology.uniform_space.basic
 -/
 universes u v
 
-open filter topological_space set classical uniform_space
+open filter topological_space set classical uniform_space function
 open_locale classical uniformity topological_space filter
 
 variables {α : Type u} {β : Type v} [uniform_space α]
@@ -176,6 +176,19 @@ lemma cauchy_seq.comp_tendsto {γ} [semilattice_sup β] [semilattice_sup γ] [no
   cauchy_seq (f ∘ g) :=
 cauchy_seq_iff_tendsto.2 $ hf.tendsto_uniformity.comp (hg.prod_at_top hg)
 
+lemma cauchy_seq.comp_injective [semilattice_sup β] [no_max_order β] [nonempty β]
+  {u : ℕ → α} (hu : cauchy_seq u) {f : β → ℕ} (hf : injective f) :
+  cauchy_seq (u ∘ f) :=
+hu.comp_tendsto $ nat.cofinite_eq_at_top ▸ hf.tendsto_cofinite.mono_left at_top_le_cofinite
+
+lemma function.bijective.cauchy_seq_comp_iff {f : ℕ → ℕ} (hf : bijective f) (u : ℕ → α) :
+  cauchy_seq (u ∘ f) ↔ cauchy_seq u :=
+begin
+  refine ⟨λ H, _, λ H, H.comp_injective hf.injective⟩,
+  lift f to ℕ ≃ ℕ using hf,
+  simpa only [(∘), f.apply_symm_apply] using H.comp_injective f.symm.injective
+end
+
 lemma cauchy_seq.subseq_subseq_mem {V : ℕ → set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α)
   {u : ℕ → α} (hu : cauchy_seq u)
   {f g : ℕ → ℕ} (hf : tendsto f at_top at_top) (hg : tendsto g at_top at_top) :