refactor(topology/subset_properties): more properties of `compact_cov…

…ering` (#6328)

Modify the definition of `compact_covering α n` to ensure that it is monotone in `n`.

Also, in a locally compact space, prove the existence of a compact exhaustion, i.e. a sequence which satisfies the properties for `compact_covering` and in which, moreover, the interior of the next set includes the previous set.

src/data/nat/basic.lean

@@ -1310,7 +1310,15 @@ by rw [pos_iff_ne_zero, not_iff_not, nat.find_eq_zero]
 
 theorem find_le (h : ∀ n, q n → p n) (hp : ∃ n, p n) (hq : ∃ n, q n) :
   nat.find hp ≤ nat.find hq :=
-nat.find_min' _ ((h _) (nat.find_spec hq))
+nat.find_min' _ (h _ (nat.find_spec hq))
+
+lemma find_comp_succ (h₁ : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h0 : ¬ p 0) :
+  nat.find h₁ = nat.find h₂ + 1 :=
+begin
+  refine (find_eq_iff _).2 ⟨nat.find_spec h₂, λ n hn, _⟩,
+  cases n with n,
+  exacts [h0, @nat.find_min (λ n, p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)]
+end
 
 end find
 

src/topology/subset_properties.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
 import topology.bases
 import data.finset.order
+import data.set.accumulate
 
 /-!
 # Properties of subsets of topological spaces
@@ -147,15 +148,24 @@ end
 
 alias compact_iff_ultrafilter_le_nhds ↔ is_compact.ultrafilter_le_nhds _
 
+/-- For every open directed cover of a compact set, there exists a single element of the 
+cover which itself includes the set. -/
+lemma is_compact.elim_directed_cover {ι : Type v} [hι : nonempty ι] (hs : is_compact s)
+  (U : ι → set α) (hUo : ∀i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) (hdU : directed (⊆) U) :
+  ∃ i, s ⊆ U i :=
+hι.elim $ λ i₀, is_compact.induction_on hs ⟨i₀, empty_subset _⟩
+  (λ s₁ s₂ hs ⟨i, hi⟩, ⟨i, subset.trans hs hi⟩)
+  (λ s₁ s₂ ⟨i, hi⟩ ⟨j, hj⟩, let ⟨k, hki, hkj⟩ := hdU i j in
+    ⟨k, union_subset (subset.trans hi hki) (subset.trans hj hkj)⟩)
+  (λ x hx, let ⟨i, hi⟩ := mem_Union.1 (hsU hx) in
+    ⟨U i, mem_nhds_within_of_mem_nhds (mem_nhds_sets (hUo i) hi), i, subset.refl _⟩)
+
 /-- For every open cover of a compact set, there exists a finite subcover. -/
 lemma is_compact.elim_finite_subcover {ι : Type v} (hs : is_compact s)
   (U : ι → set α) (hUo : ∀i, is_open (U i)) (hsU : s ⊆ ⋃ i, U i) :
   ∃ t : finset ι, s ⊆ ⋃ i ∈ t, U i :=
-is_compact.induction_on hs ⟨∅, empty_subset _⟩ (λ s₁ s₂ hs ⟨t, hs₂⟩, ⟨t, subset.trans hs hs₂⟩)
-  (λ s₁ s₂ ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩,
-    ⟨t₁ ∪ t₂, by { rw [finset.set_bUnion_union], exact union_subset_union ht₁ ht₂ }⟩)
-  (λ x hx, let ⟨i, hi⟩ := mem_Union.1 (hsU hx) in
-    ⟨U i, mem_nhds_within.2 ⟨U i, hUo i, hi, inter_subset_left _ _⟩, {i}, by simp⟩)
+hs.elim_directed_cover _ (λ t, is_open_bUnion $ λ i _, hUo i) (Union_eq_Union_finset U ▸ hsU)
+  (directed_of_sup $ λ t₁ t₂ h, bUnion_subset_bUnion_left h)
 
 /-- For every family of closed sets whose intersection avoids a compact set,
 there exists a finite subfamily whose intersection avoids this compact set. -/
@@ -326,6 +336,10 @@ lemma finset.compact_bUnion (s : finset β) {f : β → set α} (hf : ∀i ∈ s
   is_compact (⋃i ∈ s, f i) :=
 s.finite_to_set.compact_bUnion hf
 
+lemma compact_accumulate {K : ℕ → set α} (hK : ∀ n, is_compact (K n)) (n : ℕ) :
+  is_compact (accumulate K n) :=
+(finite_le_nat n).compact_bUnion $ λ k _, hK k
+
 lemma compact_Union {f : β → set α} [fintype β]
   (h : ∀i, is_compact (f i)) : is_compact (⋃i, f i) :=
 by rw ← bUnion_univ; exact finite_univ.compact_bUnion (λ i _, h i)
@@ -789,18 +803,108 @@ end
 variables (α) [sigma_compact_space α]
 open sigma_compact_space
 
-/-- An arbitrary compact covering of a σ-compact space. -/
+/-- A choice of compact covering for a σ-compact space, chosen to be monotone. -/
 def compact_covering : ℕ → set α :=
-classical.some exists_compact_covering
+accumulate exists_compact_covering.some
 
 lemma is_compact_compact_covering (n : ℕ) : is_compact (compact_covering α n) :=
-(classical.some_spec sigma_compact_space.exists_compact_covering).1 n
+compact_accumulate (classical.some_spec sigma_compact_space.exists_compact_covering).1 n
 
 lemma Union_compact_covering : (⋃ n, compact_covering α n) = univ :=
-(classical.some_spec sigma_compact_space.exists_compact_covering).2
+begin
+  rw [compact_covering, Union_accumulate],
+  exact (classical.some_spec sigma_compact_space.exists_compact_covering).2
+end
+
+@[mono] lemma compact_covering_subset ⦃m n : ℕ⦄ (h : m ≤ n) :
+  compact_covering α m ⊆ compact_covering α n :=
+monotone_accumulate h
 
 end compact
 
+/-- An [exhaustion by compact sets](https://en.wikipedia.org/wiki/Exhaustion_by_compact_sets) of a
+topological space is a sequence of compact sets `K n` such that `K n ⊆ interior (K (n + 1))` and
+`(⋃ n, K n) = univ`.
+
+If `X` is a locally compact sigma compact space, then `compact_exhaustion.choice X` provides
+a choice of an exhaustion by compact sets. This choice is also available as
+`(default : compact_exhaustion X)`. -/
+structure compact_exhaustion (X : Type*) [topological_space X] :=
+(to_fun : ℕ → set X)
+(is_compact' : ∀ n, is_compact (to_fun n))
+(subset_interior_succ' : ∀ n, to_fun n ⊆ interior (to_fun (n + 1)))
+(Union_eq' : (⋃ n, to_fun n) = univ)
+
+namespace compact_exhaustion
+
+instance : has_coe_to_fun (compact_exhaustion α) := ⟨_, to_fun⟩
+
+variables {α} (K : compact_exhaustion α)
+
+protected lemma is_compact (n : ℕ) : is_compact (K n) := K.is_compact' n
+
+lemma subset_interior_succ (n : ℕ) : K n ⊆ interior (K (n + 1)) :=
+K.subset_interior_succ' n
+
+lemma subset_succ (n : ℕ) : K n ⊆ K (n + 1) :=
+subset.trans (K.subset_interior_succ n) interior_subset
+
+@[mono] protected lemma subset ⦃m n : ℕ⦄ (h : m ≤ n) : K m ⊆ K n :=
+show K m ≤ K n, from monotone_of_monotone_nat K.subset_succ h
+
+lemma subset_interior ⦃m n : ℕ⦄ (h : m < n) : K m ⊆ interior (K n) :=
+subset.trans (K.subset_interior_succ m) $ interior_mono $ K.subset h
+
+lemma Union_eq : (⋃ n, K n) = univ := K.Union_eq'
+
+lemma exists_mem (x : α) : ∃ n, x ∈ K n := Union_eq_univ_iff.1 K.Union_eq x
+
+/-- The minimal `n` such that `x ∈ K n`. -/
+protected noncomputable def find (x : α) : ℕ := nat.find (K.exists_mem x)
+
+lemma mem_find (x : α) : x ∈ K (K.find x) := nat.find_spec (K.exists_mem x)
+
+lemma mem_iff_find_le {x : α} {n : ℕ} : x ∈ K n ↔ K.find x ≤ n :=
+⟨λ h, nat.find_min' (K.exists_mem x) h, λ h, K.subset h $ K.mem_find x⟩
+
+/-- Prepend the empty set to a compact exhaustion `K n`. -/
+def shiftr : compact_exhaustion α :=
+{ to_fun := λ n, nat.cases_on n ∅ K,
+  is_compact' := λ n, nat.cases_on n compact_empty K.is_compact,
+  subset_interior_succ' := λ n, nat.cases_on n (empty_subset _) K.subset_interior_succ,
+  Union_eq' := Union_eq_univ_iff.2 $ λ x, ⟨K.find x + 1, K.mem_find x⟩ }
+
+@[simp] lemma find_shiftr (x : α) : K.shiftr.find x = K.find x + 1 :=
+nat.find_comp_succ _ _ (not_mem_empty _)
+
+lemma mem_diff_shiftr_find (x : α) : x ∈ K.shiftr (K.find x + 1) \ K.shiftr (K.find x) :=
+⟨K.mem_find _, mt K.shiftr.mem_iff_find_le.1 $
+  by simp only [find_shiftr, not_le, nat.lt_succ_self]⟩
+
+/-- A choice of an
+[exhaustion by compact sets](https://en.wikipedia.org/wiki/Exhaustion_by_compact_sets)
+of a locally compact sigma compact space. -/
+noncomputable def choice (X : Type*) [topological_space X] [locally_compact_space X]
+  [sigma_compact_space X] : compact_exhaustion X :=
+begin
+  apply classical.choice,
+  let K : ℕ → {s : set X // is_compact s} :=
+    λ n, nat.rec_on n ⟨∅, compact_empty⟩
+      (λ n s, ⟨(exists_compact_superset s.2).some ∪ compact_covering X n,
+        (exists_compact_superset s.2).some_spec.1.union (is_compact_compact_covering _ _)⟩),
+  refine ⟨⟨λ n, K n, λ n, (K n).2, λ n, _, _⟩⟩,
+  { exact subset.trans (exists_compact_superset (K n).2).some_spec.2
+      (interior_mono $ subset_union_left _ _) },
+  { refine univ_subset_iff.1 (Union_compact_covering X ▸ _),
+    exact Union_subset_Union2 (λ n, ⟨n + 1, subset_union_right _ _⟩) }
+end
+
+noncomputable instance [locally_compact_space α] [sigma_compact_space α] :
+  inhabited (compact_exhaustion α) :=
+⟨compact_exhaustion.choice α⟩
+
+end compact_exhaustion
+
 section clopen
 
 /-- A set is clopen if it is both open and closed. -/