feat(topology/algebra/ordered): generalize real.compact_Icc (#6602)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/data/set/intervals/basic.lean

@@ -1138,6 +1138,8 @@ by simp only [Ioi_inter_Iio.symm, Ioi_inter_Ioi.symm, Iio_inter_Iio.symm]; ac_re
 
 end both
 
+lemma Icc_bot_top {α} [bounded_lattice α] : Icc (⊥ : α) ⊤ = univ := by simp
+
 end lattice
 
 section linear_order

src/order/filter/ultrafilter.lean

@@ -74,6 +74,9 @@ alias frequently_iff_eventually ↔ filter.frequently.eventually _
 
 lemma compl_mem_iff_not_mem : sᶜ ∈ f ↔ s ∉ f := by rw [← compl_not_mem_iff, compl_compl]
 
+lemma diff_mem_iff (f : ultrafilter α) : s \ t ∈ f ↔ s ∈ f ∧ t ∉ f :=
+inter_mem_sets_iff.trans $ and_congr iff.rfl compl_mem_iff_not_mem
+
 /-- If `sᶜ ∉ f ↔ s ∈ f`, then `f` is an ultrafilter. The other implication is given by
 `ultrafilter.compl_not_mem_iff`.  -/
 def of_compl_not_mem_iff (f : filter α) (h : ∀ s, sᶜ ∉ f ↔ s ∈ f) : ultrafilter α :=

src/topology/algebra/ordered.lean

@@ -2463,6 +2463,72 @@ lemma continuous_on.surj_on_of_tendsto' {f : α → β} {s : set α} [ord_connec
 
 end densely_ordered
 
+/-- A closed interval in a conditionally complete linear order is compact. -/
+lemma compact_Icc {a b : α} : is_compact (Icc a b) :=
+begin
+  cases le_or_lt a b with hab hab, swap, { simp [hab] },
+  refine compact_iff_ultrafilter_le_nhds.2 (λ f hf, _),
+  contrapose! hf,
+  rw [le_principal_iff],
+  have hpt : ∀ x ∈ Icc a b, {x} ∉ f,
+    from λ x hx hxf, hf x hx ((le_pure_iff.2 hxf).trans (pure_le_nhds x)),
+  set s := {x ∈ Icc a b | Icc a x ∉ f},
+  have hsb : b ∈ upper_bounds s, from λ x hx, hx.1.2,
+  have sbd : bdd_above s, from ⟨b, hsb⟩,
+  have ha : a ∈ s, by simp [hpt, hab],
+  rcases hab.eq_or_lt with rfl|hlt, { exact ha.2 },
+  set c := Sup s,
+  have hsc : is_lub s c, from is_lub_cSup ⟨a, ha⟩ sbd,
+  have hc : c ∈ Icc a b, from ⟨hsc.1 ha, hsc.2 hsb⟩,
+  specialize hf c hc,
+  have hcs : c ∈ s,
+  { cases hc.1.eq_or_lt with heq hlt, { rwa ← heq },
+    refine ⟨hc, λ hcf, hf (λ U hU, _)⟩,
+    rcases (mem_nhds_within_Iic_iff_exists_Ioc_subset' hlt).1 (mem_nhds_within_of_mem_nhds hU)
+      with ⟨x, hxc, hxU⟩,
+    rcases ((hsc.frequently_mem ⟨a, ha⟩).and_eventually
+      (Ioc_mem_nhds_within_Iic ⟨hxc, le_rfl⟩)).exists
+      with ⟨y, ⟨hyab, hyf⟩, hy⟩,
+    refine mem_sets_of_superset(f.diff_mem_iff.2 ⟨hcf, hyf⟩) (subset.trans _ hxU),
+    rw diff_subset_iff,
+    exact subset.trans Icc_subset_Icc_union_Ioc
+      (union_subset_union subset.rfl $ Ioc_subset_Ioc_left hy.1.le) },
+  cases hc.2.eq_or_lt with heq hlt, { rw ← heq, exact hcs.2 },
+  contrapose! hf,
+  intros U hU,
+  rcases (mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset hlt).1 (mem_nhds_within_of_mem_nhds hU)
+    with ⟨y, hxy, hyU⟩,
+  refine mem_sets_of_superset _ hyU, clear_dependent U,
+  have hy : y ∈ Icc a b, from ⟨hc.1.trans hxy.1.le, hxy.2⟩,
+  by_cases hay : Icc a y ∈ f,
+  { refine mem_sets_of_superset (f.diff_mem_iff.2 ⟨f.diff_mem_iff.2 ⟨hay, hcs.2⟩, hpt y hy⟩) _,
+    rw [diff_subset_iff, union_comm, Ico_union_right hxy.1.le, diff_subset_iff],
+    exact Icc_subset_Icc_union_Icc },
+  { exact ((hsc.1 ⟨hy, hay⟩).not_lt hxy.1).elim },
+end
+
+/-- An unordered closed interval in a conditionally complete linear order is compact. -/
+lemma compact_interval {a b : α} : is_compact (interval a b) := compact_Icc
+
+lemma compact_pi_Icc {ι : Type*} {α : ι → Type*} [Π i, conditionally_complete_linear_order (α i)]
+  [Π i, topological_space (α i)] [Π i, order_topology (α i)] (a b : Π i, α i) :
+  is_compact (Icc a b) :=
+pi_univ_Icc a b ▸ compact_univ_pi $ λ i, compact_Icc
+
+instance compact_space_Icc (a b : α) : compact_space (Icc a b) :=
+compact_iff_compact_space.mp compact_Icc
+
+instance compact_space_pi_Icc {ι : Type*} {α : ι → Type*}
+  [Π i, conditionally_complete_linear_order (α i)] [Π i, topological_space (α i)]
+  [Π i, order_topology (α i)] (a b : Π i, α i) : compact_space (Icc a b) :=
+compact_iff_compact_space.mp (compact_pi_Icc a b)
+
+@[priority 100] -- See note [lower instance priority]
+instance compact_space_of_complete_linear_order {α : Type*} [complete_linear_order α]
+  [topological_space α] [order_topology α] :
+  compact_space α :=
+⟨by simp only [← Icc_bot_top, compact_Icc]⟩
+
 lemma is_compact.Inf_mem {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
   Inf s ∈ s :=
 hs.is_closed.cInf_mem ne_s hs.bdd_below

src/topology/instances/real.lean

@@ -216,48 +216,6 @@ by rw [real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add,
   add_sub_cancel', add_self_div_two, ← add_div,
   add_assoc, add_sub_cancel'_right, add_self_div_two]
 
-lemma real.totally_bounded_Ioo (a b : ℝ) : totally_bounded (Ioo a b) :=
-metric.totally_bounded_iff.2 $ λ ε ε0, begin
-  rcases exists_nat_gt ((b - a) / ε) with ⟨n, ba⟩,
-  rw [div_lt_iff' ε0, sub_lt_iff_lt_add'] at ba,
-  let s := (λ i:ℕ, a + ε * i) '' {i:ℕ | i < n},
-  refine ⟨s, (set.finite_lt_nat _).image _, _⟩,
-  rintro x ⟨ax, xb⟩,
-  let i : ℕ := ⌊(x - a) / ε⌋.to_nat,
-  have : (i : ℤ) = ⌊(x - a) / ε⌋ :=
-    int.to_nat_of_nonneg (floor_nonneg.2 $ le_of_lt (div_pos (sub_pos.2 ax) ε0)),
-  simp, use i, split,
-  { rw [← int.coe_nat_lt, this],
-    refine int.cast_lt.1 (lt_of_le_of_lt (floor_le _) _),
-    rw [int.cast_coe_nat, div_lt_iff' ε0, sub_lt_iff_lt_add'],
-    exact lt_trans xb ba },
-  { rw [real.dist_eq, ← int.cast_coe_nat, this, abs_of_nonneg,
-        ← sub_sub, sub_lt_iff_lt_add'],
-    { have := lt_floor_add_one ((x - a) / ε),
-      rwa [div_lt_iff' ε0, mul_add, mul_one] at this },
-    { have := floor_le ((x - a) / ε),
-      rwa [sub_nonneg, ← le_sub_iff_add_le', ← le_div_iff' ε0] } }
-end
-
-lemma real.totally_bounded_ball (x ε : ℝ) : totally_bounded (ball x ε) :=
-by rw real.ball_eq_Ioo; apply real.totally_bounded_Ioo
-
-lemma real.totally_bounded_Ico (a b : ℝ) : totally_bounded (Ico a b) :=
-let ⟨c, ac⟩ := no_bot a in totally_bounded_subset
-  (by exact λ x ⟨h₁, h₂⟩, ⟨lt_of_lt_of_le ac h₁, h₂⟩)
-  (real.totally_bounded_Ioo c b)
-
-lemma real.totally_bounded_Icc (a b : ℝ) : totally_bounded (Icc a b) :=
-let ⟨c, bc⟩ := no_top b in totally_bounded_subset
-  (by exact λ x ⟨h₁, h₂⟩, ⟨h₁, lt_of_le_of_lt h₂ bc⟩)
-  (real.totally_bounded_Ico a c)
-
-lemma rat.totally_bounded_Icc (a b : ℚ) : totally_bounded (Icc a b) :=
-begin
-  have := totally_bounded_preimage uniform_embedding_of_rat (real.totally_bounded_Icc a b),
-  rwa (set.ext (λ q, _) : Icc _ _ = _), simp
-end
-
 instance : complete_space ℝ :=
 begin
   apply complete_of_cauchy_seq_tendsto,
@@ -270,6 +228,15 @@ begin
   refine this.imp (λ N hN n hn, hε (hN n hn))
 end
 
+lemma real.totally_bounded_ball (x ε : ℝ) : totally_bounded (ball x ε) :=
+by rw real.ball_eq_Ioo; apply totally_bounded_Ioo
+
+lemma rat.totally_bounded_Icc (a b : ℚ) : totally_bounded (Icc a b) :=
+begin
+  have := totally_bounded_preimage uniform_embedding_of_rat (totally_bounded_Icc a b),
+  rwa (set.ext (λ q, _) : Icc _ _ = _), simp
+end
+
 section
 
 lemma closure_of_rat_image_lt {q : ℚ} : closure ((coe:ℚ → ℝ) '' {x | q < x}) = {r | ↑q ≤ r} :=
@@ -291,20 +258,6 @@ lemma closure_of_rat_image_le_le_eq {a b : ℚ} (hab : a ≤ b) :
   closure (of_rat '' {q:ℚ | a ≤ q ∧ q ≤ b}) = {r:ℝ | of_rat a ≤ r ∧ r ≤ of_rat b} :=
 _-/
 
-lemma compact_Icc {a b : ℝ} : is_compact (Icc a b) :=
-compact_of_totally_bounded_is_closed
-  (real.totally_bounded_Icc a b)
-  (is_closed_inter (is_closed_ge' a) (is_closed_le' b))
-
-instance {a b : ℝ} : compact_space (Icc a b) :=
-compact_iff_compact_space.mp compact_Icc
-
-lemma compact_pi_Icc {ι : Type*} {a b : ι → ℝ} : is_compact (Icc a b) :=
-pi_univ_Icc a b ▸ compact_univ_pi $ λ i, compact_Icc
-
-instance compact_space_pi_Icc {ι : Type*} {a b : ι → ℝ} : compact_space (Icc a b) :=
-compact_iff_compact_space.mp compact_pi_Icc
-
 instance : proper_space ℝ :=
 { compact_ball := λx r, by rw closed_ball_Icc; apply compact_Icc }
 

src/topology/metric_space/basic.lean

@@ -869,21 +869,31 @@ theorem real.dist_0_eq_abs (x : ℝ) : dist x 0 = abs x :=
 by simp [real.dist_eq]
 
 instance : order_topology ℝ :=
-order_topology_of_nhds_abs $ λ x, begin
-  simp only [show ∀ r, {b : ℝ | abs (x - b) < r} = ball x r,
-    by simp [abs_sub, ball, real.dist_eq]],
-  apply le_antisymm,
-  { simp [le_infi_iff],
-    exact λ ε ε0, mem_nhds_sets (is_open_ball) (mem_ball_self ε0) },
-  { intros s h,
-    rcases mem_nhds_iff.1 h with ⟨ε, ε0, ss⟩,
-    exact mem_infi_sets _ (mem_infi_sets ε0 (mem_principal_sets.2 ss)) },
-end
+order_topology_of_nhds_abs $ λ x,
+  by simp only [nhds_basis_ball.eq_binfi, ball, real.dist_eq, abs_sub]
 
 lemma closed_ball_Icc {x r : ℝ} : closed_ball x r = Icc (x-r) (x+r) :=
 by ext y; rw [mem_closed_ball, dist_comm, real.dist_eq,
   abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add', sub_le]
 
+section metric_ordered
+
+variables [conditionally_complete_linear_order α] [order_topology α]
+
+lemma totally_bounded_Icc (a b : α) : totally_bounded (Icc a b) :=
+compact_Icc.totally_bounded
+
+lemma totally_bounded_Ico (a b : α) : totally_bounded (Ico a b) :=
+totally_bounded_subset Ico_subset_Icc_self (totally_bounded_Icc a b)
+
+lemma totally_bounded_Ioc (a b : α) : totally_bounded (Ioc a b) :=
+totally_bounded_subset Ioc_subset_Icc_self (totally_bounded_Icc a b)
+
+lemma totally_bounded_Ioo (a b : α) : totally_bounded (Ioo a b) :=
+totally_bounded_subset Ioo_subset_Icc_self (totally_bounded_Icc a b)
+
+end metric_ordered
+
 /-- Special case of the sandwich theorem; see `tendsto_of_tendsto_of_tendsto_of_le_of_le'` for the
 general case. -/
 lemma squeeze_zero' {α} {f g : α → ℝ} {t₀ : filter α} (hf : ∀ᶠ t in t₀, 0 ≤ f t)

src/topology/uniform_space/cauchy.lean

@@ -412,6 +412,12 @@ lemma compact_iff_totally_bounded_complete {s : set α} :
  λ ⟨ht, hc⟩, compact_iff_ultrafilter_le_nhds.2
    (λf hf, hc _ (totally_bounded_iff_ultrafilter.1 ht f hf) hf)⟩
 
+lemma is_compact.totally_bounded {s : set α} (h : is_compact s) : totally_bounded s :=
+(compact_iff_totally_bounded_complete.1 h).1
+
+lemma is_compact.is_complete {s : set α} (h : is_compact s) : is_complete s :=
+(compact_iff_totally_bounded_complete.1 h).2
+
 @[priority 100] -- see Note [lower instance priority]
 instance complete_of_compact {α : Type u} [uniform_space α] [compact_space α] : complete_space α :=
 ⟨λf hf, by simpa using (compact_iff_totally_bounded_complete.1 compact_univ).2 f hf⟩