feat(order/filter,topology/instances/real): lemmas about at_top, at_bot, and cocompact (#10652)

* prove `comap abs at_top = at_bot ⊔ at_top`;
* prove `comap coe at_top = at_top` and `comap coe at_bot = at_bot` for coercion from `ℕ`, `ℤ`, or `ℚ` to an archimedian semiring, ring, or field, respectively;
* prove `cocompact ℤ = at_bot ⊔ at_top` and `cocompact ℝ = at_bot ⊔ at_top`.

Author: urkud

src/algebra/order/group.lean

@@ -1125,8 +1125,9 @@ section linear_ordered_add_comm_group
 
 variables [linear_ordered_add_comm_group α] {a b c d : α}
 
-lemma abs_le : |a| ≤ b ↔ - b ≤ a ∧ a ≤ b :=
-by rw [abs_le', and.comm, neg_le]
+lemma abs_le : |a| ≤ b ↔ - b ≤ a ∧ a ≤ b := by rw [abs_le', and.comm, neg_le]
+
+lemma le_abs' : a ≤ |b| ↔ b ≤ -a ∨ a ≤ b := by rw [le_abs, or.comm, le_neg]
 
 lemma neg_le_of_abs_le (h : |a| ≤ b) : -b ≤ a := (abs_le.mp h).1
 

src/order/filter/archimedean.lean

@@ -19,6 +19,10 @@ variables {α R : Type*}
 
 open filter set
 
+@[simp] lemma nat.comap_coe_at_top [ordered_semiring R] [nontrivial R] [archimedean R] :
+  comap (coe : ℕ → R) at_top = at_top :=
+comap_embedding_at_top (λ _ _, nat.cast_le) exists_nat_ge
+
 lemma tendsto_coe_nat_at_top_iff [ordered_semiring R] [nontrivial R] [archimedean R]
   {f : α → ℕ} {l : filter α} :
   tendsto (λ n, (f n : R)) l at_top ↔ tendsto f l at_top :=
@@ -28,22 +32,48 @@ lemma tendsto_coe_nat_at_top_at_top [ordered_semiring R] [archimedean R] :
   tendsto (coe : ℕ → R) at_top at_top :=
 nat.mono_cast.tendsto_at_top_at_top exists_nat_ge
 
+@[simp] lemma int.comap_coe_at_top [ordered_ring R] [nontrivial R] [archimedean R] :
+  comap (coe : ℤ → R) at_top = at_top :=
+comap_embedding_at_top (λ _ _, int.cast_le) $ λ r, let ⟨n, hn⟩ := exists_nat_ge r in ⟨n, hn⟩
+
+@[simp] lemma int.comap_coe_at_bot [ordered_ring R] [nontrivial R] [archimedean R] :
+  comap (coe : ℤ → R) at_bot = at_bot :=
+comap_embedding_at_bot (λ _ _, int.cast_le) $ λ r,
+  let ⟨n, hn⟩ := exists_nat_ge (-r) in ⟨-n, by simpa [neg_le] using hn⟩
+
 lemma tendsto_coe_int_at_top_iff [ordered_ring R] [nontrivial R] [archimedean R]
   {f : α → ℤ} {l : filter α} :
   tendsto (λ n, (f n : R)) l at_top ↔ tendsto f l at_top :=
-tendsto_at_top_embedding (assume a₁ a₂, int.cast_le) $
-  assume r, let ⟨n, hn⟩ := exists_nat_ge r in ⟨(n:ℤ), hn⟩
+by rw [← tendsto_comap_iff, int.comap_coe_at_top]
+
+lemma tendsto_coe_int_at_bot_iff [ordered_ring R] [nontrivial R] [archimedean R]
+  {f : α → ℤ} {l : filter α} :
+  tendsto (λ n, (f n : R)) l at_bot ↔ tendsto f l at_bot :=
+by rw [← tendsto_comap_iff, int.comap_coe_at_bot]
 
 lemma tendsto_coe_int_at_top_at_top [ordered_ring R] [archimedean R] :
   tendsto (coe : ℤ → R) at_top at_top :=
 int.cast_mono.tendsto_at_top_at_top $ λ b,
   let ⟨n, hn⟩ := exists_nat_ge b in ⟨n, hn⟩
 
+@[simp] lemma rat.comap_coe_at_top [linear_ordered_field R] [archimedean R] :
+  comap (coe : ℚ → R) at_top = at_top :=
+comap_embedding_at_top (λ _ _, rat.cast_le) $ λ r, let ⟨n, hn⟩ := exists_nat_ge r in ⟨n, by simpa⟩
+
+@[simp] lemma rat.comap_coe_at_bot [linear_ordered_field R] [archimedean R] :
+  comap (coe : ℚ → R) at_bot = at_bot :=
+comap_embedding_at_bot (λ _ _, rat.cast_le) $ λ r, let ⟨n, hn⟩ := exists_nat_ge (-r)
+  in ⟨-n, by simpa [neg_le]⟩
+
 lemma tendsto_coe_rat_at_top_iff [linear_ordered_field R] [archimedean R]
   {f : α → ℚ} {l : filter α} :
   tendsto (λ n, (f n : R)) l at_top ↔ tendsto f l at_top :=
-tendsto_at_top_embedding (assume a₁ a₂, rat.cast_le) $
-  assume r, let ⟨n, hn⟩ := exists_nat_ge r in ⟨(n:ℚ), by assumption_mod_cast⟩
+by rw [← tendsto_comap_iff, rat.comap_coe_at_top]
+
+lemma tendsto_coe_rat_at_bot_iff [linear_ordered_field R] [archimedean R]
+  {f : α → ℚ} {l : filter α} :
+  tendsto (λ n, (f n : R)) l at_bot ↔ tendsto f l at_bot :=
+by rw [← tendsto_comap_iff, rat.comap_coe_at_bot]
 
 lemma at_top_countable_basis_of_archimedean [linear_ordered_semiring R] [archimedean R] :
   (at_top : filter R).has_countable_basis (λ n : ℕ, true) (λ n, Ici n) :=

src/order/filter/at_top_bot.lean

@@ -635,6 +635,16 @@ tendsto_at_top_mono le_abs_self tendsto_id
 lemma tendsto_abs_at_bot_at_top : tendsto (abs : α → α) at_bot at_top :=
 tendsto_at_top_mono neg_le_abs_self tendsto_neg_at_bot_at_top
 
+@[simp] lemma comap_abs_at_top : comap (abs : α → α) at_top = at_bot ⊔ at_top :=
+begin
+  refine le_antisymm (((at_top_basis.comap _).le_basis_iff (at_bot_basis.sup at_top_basis)).2 _)
+    (sup_le tendsto_abs_at_bot_at_top.le_comap tendsto_abs_at_top_at_top.le_comap),
+  rintro ⟨a, b⟩ -,
+  refine ⟨max (-a) b, trivial, λ x hx, _⟩,
+  rw [mem_preimage, mem_Ici, le_abs', max_le_iff, ← min_neg_neg, le_min_iff, neg_neg] at hx,
+  exact hx.imp and.left and.right
+end
+
 end linear_ordered_add_comm_group
 
 section linear_ordered_semiring
@@ -828,15 +838,23 @@ alias tendsto_at_bot_at_bot_of_monotone ← monotone.tendsto_at_bot_at_bot
 alias tendsto_at_top_at_top_iff_of_monotone ← monotone.tendsto_at_top_at_top_iff
 alias tendsto_at_bot_at_bot_iff_of_monotone ← monotone.tendsto_at_bot_at_bot_iff
 
+lemma comap_embedding_at_top [preorder β] [preorder γ] {e : β → γ}
+  (hm : ∀b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀c, ∃b, c ≤ e b) :
+  comap e at_top = at_top :=
+le_antisymm
+  (le_infi $ λ b, le_principal_iff.2 $ mem_comap.2 ⟨Ici (e b), mem_at_top _, λ x, (hm _ _).1⟩)
+  (tendsto_at_top_at_top_of_monotone (λ _ _, (hm _ _).2) hu).le_comap
+
+lemma comap_embedding_at_bot [preorder β] [preorder γ] {e : β → γ}
+  (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀c, ∃b, e b ≤ c) :
+  comap e at_bot = at_bot :=
+@comap_embedding_at_top (order_dual β) (order_dual γ) _ _ e (function.swap hm) hu
+
 lemma tendsto_at_top_embedding [preorder β] [preorder γ]
   {f : α → β} {e : β → γ} {l : filter α}
   (hm : ∀b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀c, ∃b, c ≤ e b) :
   tendsto (e ∘ f) l at_top ↔ tendsto f l at_top :=
-begin
-  refine ⟨_, (tendsto_at_top_at_top_of_monotone (λ b₁ b₂, (hm b₁ b₂).2) hu).comp⟩,
-  rw [tendsto_at_top, tendsto_at_top],
-  exact λ hc b, (hc (e b)).mono (λ a, (hm b (f a)).1)
-end
+by rw [← comap_embedding_at_top hm hu, tendsto_comap_iff]
 
 /-- A function `f` goes to `-∞` independent of an order-preserving embedding `e`. -/
 lemma tendsto_at_bot_embedding [preorder β] [preorder γ]

src/topology/instances/real.lean

@@ -9,6 +9,7 @@ import topology.algebra.ring
 import ring_theory.subring.basic
 import group_theory.archimedean
 import algebra.periodic
+import order.filter.archimedean
 
 /-!
 # Topological properties of ℝ
@@ -98,13 +99,12 @@ instance : proper_space ℤ :=
     exact (set.finite_Icc _ _).is_compact,
   end ⟩
 
+@[simp] lemma cocompact_eq : cocompact ℤ = at_bot ⊔ at_top :=
+by simp only [← comap_dist_right_at_top_eq_cocompact (0 : ℤ), dist_eq, sub_zero, cast_zero,
+  ← cast_abs, ← @comap_comap _ _ _ _ abs, int.comap_coe_at_top, comap_abs_at_top]
+
 instance : noncompact_space ℤ :=
-begin
-  rw [← not_compact_space_iff, metric.compact_space_iff_bounded_univ],
-  rintro ⟨r, hr⟩,
-  refine (hr (⌊r⌋ + 1) 0 trivial trivial).not_lt _,
-  simpa [dist_eq] using (lt_floor_add_one r).trans_le (le_abs_self _)
-end
+noncompact_space_of_ne_bot $ by simp [at_top_ne_bot]
 
 end int
 
@@ -160,6 +160,10 @@ is_topological_basis_of_open_of_nhds
       by { simp only [mem_Union], exact ⟨q, p, rat.cast_lt.1 $ hqa.trans hap, rfl⟩ },
       ⟨hqa, hap⟩, assume a' ⟨hqa', ha'p⟩, h ⟨hlq.trans hqa', ha'p.trans hpu⟩⟩)
 
+@[simp] lemma real.cocompact_eq : cocompact ℝ = at_bot ⊔ at_top :=
+by simp only [← comap_dist_right_at_top_eq_cocompact (0 : ℝ), real.dist_eq, sub_zero,
+  comap_abs_at_top]
+
 /- TODO(Mario): Prove that these are uniform isomorphisms instead of uniform embeddings
 lemma uniform_embedding_add_rat {r : ℚ} : uniform_embedding (λp:ℚ, p + r) :=
 _