feat(topology): sequential compactness (#3061)

This is the long overdue PR bringing Bolzano-Weierstrass to mathlib. I'm sorry it's a bit large. I did use a couple of preliminary PRs, that one is really about converging subsequences, but supporting material is spread in many files.



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

src/data/nat/basic.lean

@@ -390,6 +390,15 @@ mt (congr_arg (%2)) (by rw [add_comm, add_mul_mod_self_left, mul_mod_right]; exa
 protected def strong_rec' {p : ℕ → Sort u} (H : ∀ n, (∀ m, m < n → p m) → p n) : ∀ (n : ℕ), p n
 | n := H n (λ m hm, strong_rec' m)
 
+/-- Recursion principle based on `<` applied to some natural number. -/
+@[elab_as_eliminator]
+def strong_rec_on' {P : ℕ → Sort*} (n : ℕ) (h : ∀ n, (∀ m, m < n → P m) → P n) : P n :=
+nat.strong_rec' h n
+
+theorem strong_rec_on_beta' {P : ℕ → Sort*} {h} {n : ℕ} :
+  (strong_rec_on' n h : P n) = h n (λ m hmn, (strong_rec_on' m h : P m)) :=
+by { simp only [strong_rec_on'], rw nat.strong_rec' }
+
 attribute [simp] nat.div_self
 
 protected lemma div_le_of_le_mul' {m n : ℕ} {k} (h : m ≤ k * n) : m / k ≤ n :=

src/data/set/finite.lean

@@ -396,6 +396,33 @@ let ⟨I, Ifin, hI⟩ := finite_subset_Union tfin h in
         exact H }
     end⟩
 
+instance nat.fintype_Iio (n : ℕ) : fintype (Iio n) :=
+fintype.of_finset (finset.range n) $ by simp
+
+/--
+If `P` is some relation between terms of `γ` and sets in `γ`, 
+such that every finite set `t : set γ` has some `c : γ` related to it, 
+then there is a recursively defined sequence `u` in `γ` 
+so `u n` is related to the image of `{0, 1, ..., n-1}` under `u`.
+
+(We use this later to show sequentially compact sets
+are totally bounded.)
+-/
+lemma seq_of_forall_finite_exists  {γ : Type*}
+  {P : γ → set γ → Prop} (h : ∀ t,  finite t → ∃ c, P c t) :
+  ∃ u : ℕ → γ, ∀ n, P (u n) (u '' Iio n) :=
+⟨λ n, @nat.strong_rec_on' (λ _, γ) n $ λ n ih, classical.some $ h
+    (range $ λ m : Iio n, ih m.1 m.2)
+    (finite_range _),
+λ n, begin
+  classical,
+  refine nat.strong_rec_on' n (λ n ih, _),
+  rw nat.strong_rec_on_beta', convert classical.some_spec (h _ _),
+  ext x, split,
+  { rintros ⟨m, hmn, rfl⟩, exact ⟨⟨m, hmn⟩, rfl⟩ },
+  { rintros ⟨⟨m, hmn⟩, rfl⟩, exact ⟨m, hmn, rfl⟩ }
+end⟩
+
 lemma finite_range_ite {p : α → Prop} [decidable_pred p] {f g : α → β} (hf : finite (range f))
   (hg : finite (range g)) : finite (range (λ x, if p x then f x else g x)) :=
 finite_subset (finite_union hf hg) range_ite_subset

src/data/set/lattice.lean

@@ -262,6 +262,21 @@ theorem bInter_subset_bInter_right {s : set α} {t1 t2 : α → set β}
   (h : ∀ x ∈ s, t1 x ⊆ t2 x) : (⋂ x ∈ s, t1 x) ⊆ (⋂ x ∈ s, t2 x) :=
 subset_bInter (λ x xs, subset.trans (bInter_subset_of_mem xs) (h x xs))
 
+theorem bUnion_subset_bUnion {γ : Type*} {s : set α} {t : α → set β} {s' : set γ} {t' : γ → set β}
+  (h : ∀ x ∈ s, ∃ y ∈ s', t x ⊆ t' y) :
+  (⋃ x ∈ s, t x) ⊆ (⋃ y ∈ s', t' y) :=
+begin
+  intros x,
+  simp only [mem_Union],
+  rintros ⟨a, a_in, ha⟩,
+  rcases h a a_in with ⟨c, c_in, hc⟩,
+  exact ⟨c, c_in, hc ha⟩
+end
+
+theorem bUnion_mono {s : set α} {t t' : α → set β} (h : ∀ x ∈ s, t x ⊆ t' x) :
+  (⋃ x ∈ s, t x) ⊆ (⋃ x ∈ s, t' x) :=
+bUnion_subset_bUnion (λ x x_in, ⟨x, x_in, h x x_in⟩)
+
 theorem bUnion_eq_Union (s : set α) (t : α → set β) : (⋃ x ∈ s, t x) = (⋃ x : s, t x.1) :=
 set.ext $ by simp
 

src/order/basic.lean

@@ -139,6 +139,9 @@ protected theorem iterate [has_lt α] {f : α → α} (hf : strict_mono f) (n :
   strict_mono (f^[n]) :=
 nat.rec_on n strict_mono_id (λ n ihn, ihn.comp hf)
 
+lemma id_le {φ : ℕ → ℕ} (h : strict_mono φ) : ∀ n, n ≤ φ n :=
+λ n, nat.rec_on n (nat.zero_le _) (λ n hn, nat.succ_le_of_lt (lt_of_le_of_lt hn $ h $ nat.lt_succ_self n))
+
 section
 variables [linear_order α] [preorder β] {f : α → β}
 

src/order/filter/bases.lean

@@ -646,6 +646,25 @@ lemma tendsto_of_seq_tendsto {f : α → β} {k : filter α} {l : filter β}
   (∀ x : ℕ → α, tendsto x at_top k → tendsto (f ∘ x) at_top l) → tendsto f k l :=
 hcb.tendsto_iff_seq_tendsto.2
 
+lemma subseq_tendsto {f : filter α} (hf : is_countably_generated f)
+  {u : ℕ → α}
+  (hx : map u at_top ⊓ f ≠ ⊥) :
+  ∃ (θ : ℕ → ℕ), (strict_mono θ) ∧ (tendsto (u ∘ θ) at_top f) :=
+begin
+  rcases hf.has_antimono_basis with ⟨B, h⟩,
+  have : ∀ N, ∃ n ≥ N, u n ∈ B N,
+    from λ N, filter.map_at_top_inf_ne_bot_iff.mp hx _ (h.to_has_basis.mem_of_mem trivial) N,
+  choose φ hφ using this,
+  cases forall_and_distrib.mp hφ with φ_ge φ_in,
+  have lim_uφ : tendsto (u ∘ φ) at_top f,
+    from h.tendsto φ_in,
+  have lim_φ : tendsto φ at_top at_top,
+    from (tendsto_at_top_mono _ φ_ge tendsto_id),
+  obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, strict_mono ψ ∧ strict_mono (φ ∘ ψ),
+    from strict_mono_subseq_of_tendsto_at_top lim_φ,
+  exact ⟨φ ∘ ψ, hψφ, lim_uφ.comp $ strict_mono_tendsto_at_top hψ⟩,
+end
+
 end is_countably_generated
 
 -- TODO : prove this for a encodable type

src/order/filter/basic.lean

@@ -861,6 +861,10 @@ begin
   exact hf this
 end
 
+lemma frequently_of_forall {f : filter α} (hf : f ≠ ⊥) {p : α → Prop} (h : ∀ x, p x) :
+  ∃ᶠ x in f, p x :=
+eventually.frequently hf (f.eventually_of_forall h)
+
 lemma frequently.mp {p q : α → Prop} {f : filter α} (h : ∃ᶠ x in f, p x)
   (hpq : ∀ᶠ x in f, p x → q x) :
   ∃ᶠ x in f, q x :=
@@ -2037,11 +2041,114 @@ lemma tendsto_at_top_mono [preorder β] (l : filter α) :
   monotone (λ f : α → β, tendsto f l at_top) :=
 λ f₁ f₂ h, tendsto_at_top_mono' l $ univ_mem_sets' h
 
+/-!
+### Sequences
+-/
+
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma map_at_top_inf_ne_bot_iff [semilattice_sup α] [nonempty α] {F : filter β} {u : α → β} :
   (map u at_top) ⊓ F ≠ ⊥ ↔ ∀ U ∈ F, ∀ N, ∃ n ≥ N, u n ∈ U :=
 by simp_rw [inf_ne_bot_iff_frequently_right, frequently_map, frequently_at_top] ; trivial
 
+lemma extraction_of_frequently_at_top' {P : ℕ → Prop} (h : ∀ N, ∃ n > N, P n) :
+  ∃ φ : ℕ → ℕ, strict_mono φ ∧ ∀ n, P (φ n) :=
+begin
+  choose u hu using h,
+  cases forall_and_distrib.mp hu with hu hu',
+  exact ⟨u ∘ (nat.rec 0 (λ n v, u v)), strict_mono.nat (λ n, hu _), λ n, hu' _⟩,
+end
+
+lemma extraction_of_frequently_at_top {P : ℕ → Prop} (h : ∃ᶠ n in at_top, P n) :
+  ∃ φ : ℕ → ℕ, strict_mono φ ∧ ∀ n, P (φ n) :=
+begin
+  rw frequently_at_top' at h,
+  exact extraction_of_frequently_at_top' h,
+end
+
+lemma extraction_of_eventually_at_top {P : ℕ → Prop} (h : ∀ᶠ n in at_top, P n) :
+  ∃ φ : ℕ → ℕ, strict_mono φ ∧ ∀ n, P (φ n) :=
+extraction_of_frequently_at_top (eventually.frequently at_top_ne_bot h)
+
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma exists_le_of_tendsto_at_top [semilattice_sup α] [preorder β] {u : α → β}
+  (h : tendsto u at_top at_top) : ∀ a b, ∃ a' ≥ a, b ≤ u a' :=
+begin
+  intros a b,
+  have : ∀ᶠ x in at_top, a ≤ x ∧ b ≤ u x := inter_mem_sets (mem_at_top a) (h $ mem_at_top b),
+  haveI : nonempty α := ⟨a⟩,
+  rcases this.exists at_top_ne_bot with ⟨a', ha, hb⟩,
+  exact ⟨a', ha, hb⟩
+end
+
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma exists_lt_of_tendsto_at_top [semilattice_sup α] [preorder β] [no_top_order β]
+  {u : α → β} (h : tendsto u at_top at_top) : ∀ a b, ∃ a' ≥ a, b < u a' :=
+begin
+  intros a b,
+  cases no_top b with b' hb',
+  rcases exists_le_of_tendsto_at_top h a b' with ⟨a', ha', ha''⟩,
+  exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩
+end
+
+/--
+If `u` is a sequence which is unbounded above,
+then after any point, it reaches a value strictly greater than all previous values.
+-/
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma high_scores [linear_order β] [no_top_order β] {u : ℕ → β}
+  (hu : tendsto u at_top at_top) : ∀ N, ∃ n ≥ N, ∀ k < n, u k < u n :=
+begin
+  letI := classical.DLO β,
+  intros N,
+  let A := finset.image u (finset.range $ N+1), -- A = {u 0, ..., u N}
+  have Ane : A.nonempty,
+    from ⟨u 0, finset.mem_image_of_mem _ (finset.mem_range.mpr $ nat.zero_lt_succ _)⟩,
+  let M := finset.max' A Ane,
+  have ex : ∃ n ≥ N, M < u n,
+    from exists_lt_of_tendsto_at_top hu _ _,
+  obtain ⟨n, hnN, hnM, hn_min⟩ : ∃ n, N ≤ n ∧ M < u n ∧ ∀ k, N ≤ k → k < n → u k ≤ M,
+  { use nat.find ex,
+    rw ← and_assoc,
+    split,
+    { simpa using nat.find_spec ex },
+    { intros k hk hk',
+      simpa [hk] using nat.find_min ex hk' } },
+  use [n, hnN],
+  intros k hk,
+  by_cases H : k ≤ N,
+  { have : u k ∈ A,
+      from finset.mem_image_of_mem _ (finset.mem_range.mpr $ nat.lt_succ_of_le H),
+    have : u k ≤ M,
+      from finset.le_max' A Ane (u k) this,
+    exact lt_of_le_of_lt this hnM },
+  { push_neg at H,
+    calc u k ≤ M   : hn_min k (le_of_lt H) hk
+         ... < u n : hnM },
+end
+
+/--
+If `u` is a sequence which is unbounded above,
+then it `frequently` reaches a value strictly greater than all previous values.
+-/
+lemma frequently_high_scores [linear_order β] [no_top_order β] {u : ℕ → β}
+  (hu : tendsto u at_top at_top) : ∃ᶠ n in at_top, ∀ k < n, u k < u n :=
+by simpa [frequently_at_top] using high_scores hu
+
+lemma strict_mono_subseq_of_tendsto_at_top
+  {β : Type*} [linear_order β] [no_top_order β]
+  {u : ℕ → β} (hu : tendsto u at_top at_top) :
+  ∃ φ : ℕ → ℕ, strict_mono φ ∧ strict_mono (u ∘ φ) :=
+let ⟨φ, h, h'⟩ := extraction_of_frequently_at_top (frequently_high_scores hu) in
+⟨φ, h, λ n m hnm, h' m _ (h hnm)⟩
+
+lemma strict_mono_subseq_of_id_le {u : ℕ → ℕ} (hu : ∀ n, n ≤ u n) :
+  ∃ φ : ℕ → ℕ, strict_mono φ ∧ strict_mono (u ∘ φ) :=
+strict_mono_subseq_of_tendsto_at_top (tendsto_at_top_mono _ hu tendsto_id)
+
+lemma strict_mono_tendsto_at_top {φ : ℕ → ℕ} (h : strict_mono φ) :
+  tendsto φ at_top at_top :=
+tendsto_at_top_mono _ h.id_le tendsto_id
+
 section ordered_add_monoid
 
 variables [ordered_cancel_add_comm_monoid β] (l : filter α) {f g : α → β}

src/tactic/monotonicity/lemmas.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Simon Hudon
 -/
 import tactic.monotonicity.basic
+import data.set.lattice
 
 variables {α : Type*}
 
@@ -65,3 +66,7 @@ begin
   rw [nat.sub_add_cancel h''],
   apply nat.add_lt_add_left h
 end
+
+open set
+
+attribute [mono] monotone_inter monotone_union bUnion_mono sUnion_mono seq_mono monotone_prod

src/topology/bases.lean

@@ -116,6 +116,13 @@ class separable_space : Prop :=
 class first_countable_topology : Prop :=
 (nhds_generated_countable : ∀a:α, (𝓝 a).is_countably_generated)
 
+namespace first_countable_topology
+variable {α}
+lemma tendsto_subseq [first_countable_topology α] {u : ℕ → α} {x : α} (hx : map u at_top ⊓ 𝓝 x ≠ ⊥) :
+  ∃ (ψ : ℕ → ℕ), (strict_mono ψ) ∧ (tendsto (u ∘ ψ) at_top (𝓝 x)) :=
+(nhds_generated_countable x).subseq_tendsto hx
+end first_countable_topology
+
 /-- A second-countable space is one with a countable basis. -/
 class second_countable_topology : Prop :=
 (is_open_generated_countable [] : ∃b:set (set α), countable b ∧ t = topological_space.generate_from b)

src/topology/metric_space/basic.lean

@@ -250,6 +250,13 @@ def ball (x : α) (ε : ℝ) : set α := {y | dist y x < ε}
 
 theorem mem_ball' : y ∈ ball x ε ↔ dist x y < ε := by rw dist_comm; refl
 
+lemma ball_eq_ball (ε : ℝ) (x : α) :
+  uniform_space.ball x {p | dist p.2 p.1 < ε} = metric.ball x ε := rfl
+
+lemma ball_eq_ball' (ε : ℝ) (x : α) :
+  uniform_space.ball x {p | dist p.1 p.2 < ε} = metric.ball x ε :=
+by { ext, simp [dist_comm, uniform_space.ball] }
+
 /-- `closed_ball x ε` is the set of all points `y` with `dist y x ≤ ε` -/
 def closed_ball (x : α) (ε : ℝ) := {y | dist y x ≤ ε}
 
@@ -456,7 +463,7 @@ theorem totally_bounded_iff {s : set α} :
 /-- A metric space space is totally bounded if one can reconstruct up to any ε>0 any element of the
 space from finitely many data. -/
 @[nolint ge_or_gt] -- see Note [nolint_ge]
-lemma totally_bounded_of_finite_discretization {α : Type u} [metric_space α] {s : set α}
+lemma totally_bounded_of_finite_discretization {s : set α}
   (H : ∀ε > (0 : ℝ), ∃ (β : Type u) [fintype β] (F : s → β),
     ∀x y, F x = F y → dist (x:α) y < ε) :
   totally_bounded s :=
@@ -475,6 +482,15 @@ begin
   exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩
 end
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+theorem finite_approx_of_totally_bounded {s : set α} (hs : totally_bounded s) :
+  ∀ ε > 0, ∃ t ⊆ s, finite t ∧ s ⊆ ⋃y∈t, ball y ε :=
+begin
+  intros ε ε_pos,
+  rw totally_bounded_iff_subset at hs,
+  exact hs _ (dist_mem_uniformity ε_pos),
+end
+
 /-- Expressing locally uniform convergence on a set using `dist`. -/
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma tendsto_locally_uniformly_on_iff {ι : Type*} [topological_space β]
@@ -1410,6 +1426,24 @@ begin
   { exact bounded_closed_ball.subset hC }
 end
 
+lemma bounded_closure_of_bounded (h : bounded s) : bounded (closure s) :=
+begin
+  cases h with C h,
+  replace h : ∀ p : α × α, p ∈ set.prod s s → dist p.1 p.2 ∈ { d | d ≤ C },
+  { rintros ⟨x, y⟩ ⟨x_in, y_in⟩,
+    exact h x y x_in y_in },
+  use C,
+  suffices : ∀ p : α × α, p ∈ closure (set.prod s s) → dist p.1 p.2 ∈ { d | d ≤ C },
+  { rw closure_prod_eq at this,
+    intros x y x_in y_in,
+    exact this (x, y) (mk_mem_prod x_in y_in) },
+  intros p p_in,
+  have := mem_closure continuous_dist p_in h,
+  rwa closure_eq_of_is_closed (is_closed_le' C) at this
+end
+
+alias bounded_closure_of_bounded ← bounded.closure
+
 /-- The union of two bounded sets is bounded iff each of the sets is bounded -/
 @[simp] lemma bounded_union :
   bounded (s ∪ t) ↔ bounded s ∧ bounded t :=