feat(topology): an is_complete set is a complete_space (#2037)

* feat(*): misc simple lemmas

* +1 lemma

* Rename `inclusion_range` to `range_inclusion`

Co-Authored-By: Johan Commelin <johan@commelin.net>

* feat(topology): an `is_complete` set is a `complete_space`

Also simplify a proof in `topology/metric_space/closeds`.

* Use in `finite_dimension`

Co-authored-by: Johan Commelin <johan@commelin.net>

src/analysis/normed_space/finite_dimension.lean

@@ -99,23 +99,14 @@ begin
     { assume s s_dim,
       rcases exists_is_basis_finite 𝕜 s with ⟨b, b_basis, b_finite⟩,
       letI : fintype b := finite.fintype b_finite,
-      have U : uniform_embedding (equiv_fun_basis b_basis).symm,
+      have U : uniform_embedding (equiv_fun_basis b_basis).symm.to_equiv,
       { have : fintype.card b = n,
           by { rw ← s_dim, exact (findim_eq_card_basis b_basis).symm },
         have : continuous (equiv_fun_basis b_basis) := IH (subtype.val : b → s) this b_basis,
         exact (equiv_fun_basis b_basis).symm.uniform_embedding (linear_map.continuous_on_pi _) this },
-      have : is_complete (range ((equiv_fun_basis b_basis).symm)),
-      { rw [← image_univ, is_complete_image_iff U],
-        convert complete_univ,
-        change complete_space (b → 𝕜),
-        apply_instance },
-      have : is_complete (range (subtype.val : s → E)),
-      { change is_complete (range ((equiv_fun_basis b_basis).symm.to_equiv)) at this,
-        rw equiv.range_eq_univ at this,
-        rwa [← image_univ, is_complete_image_iff],
-        exact isometry_subtype_val.uniform_embedding },
-      apply is_closed_of_is_complete,
-      rwa subtype.val_range at this },
+      have : is_complete (s : set E),
+        from complete_space_coe_iff_is_complete.1 ((complete_space_congr U).1 (by apply_instance)),
+      exact is_closed_of_is_complete this },
     -- second step: any linear form is continuous, as its kernel is closed by the first step
     have H₂ : ∀f : E →ₗ[𝕜] 𝕜, continuous f,
     { assume f,
@@ -204,10 +195,8 @@ begin
   have : uniform_embedding (equiv_fun_basis b_basis).symm :=
     linear_equiv.uniform_embedding _ (linear_map.continuous_of_finite_dimensional _)
     (linear_map.continuous_of_finite_dimensional _),
-  have : is_complete ((equiv_fun_basis b_basis).symm.to_equiv '' univ) :=
-    (is_complete_image_iff this).mpr complete_univ,
-  rw [image_univ, equiv.range_eq_univ] at this,
-  exact complete_space_of_is_complete_univ this
+  change uniform_embedding (equiv_fun_basis b_basis).symm.to_equiv at this,
+  exact (complete_space_congr this).1 (by apply_instance)
 end
 
 variables {𝕜 E}

src/topology/metric_space/closeds.lean

@@ -245,33 +245,17 @@ isometry.uniform_embedding $ λx y, rfl
 
 /-- The range of `nonempty_compacts.to_closeds` is closed in a complete space -/
 lemma nonempty_compacts.is_closed_in_closeds [complete_space α] :
-  is_closed (nonempty_compacts.to_closeds '' (univ : set (nonempty_compacts α))) :=
+  is_closed (range $ @nonempty_compacts.to_closeds α _ _) :=
 begin
-  have : nonempty_compacts.to_closeds '' univ = {s : closeds α | s.val.nonempty ∧ compact s.val},
-  { ext,
-    simp only [set.image_univ, set.mem_range, ne.def, set.mem_set_of_eq],
-    split,
-    { rintros ⟨y, hy⟩,
-      have : x.val = y.val := by rcases hy; simp,
-      rw this,
-      exact y.property },
-    { rintros ⟨hx1, hx2⟩,
-      existsi (⟨x.val, ⟨hx1, hx2⟩⟩ : nonempty_compacts α),
-      apply subtype.eq,
-      refl }},
+  have : range nonempty_compacts.to_closeds = {s : closeds α | s.val.nonempty ∧ compact s.val},
+    from range_inclusion _,
   rw this,
-  refine is_closed_of_closure_subset (λs hs, _),
-  split,
-  { -- take a set set t which is nonempty and at distance at most 1 of s
-    rcases mem_closure_iff.1 hs 1 ennreal.zero_lt_one with ⟨t, ht, Dst⟩,
+  refine is_closed_of_closure_subset (λs hs, ⟨_, _⟩),
+  { -- take a set set t which is nonempty and at a finite distance of s
+    rcases mem_closure_iff.1 hs ⊤ ennreal.coe_lt_top with ⟨t, ht, Dst⟩,
     rw edist_comm at Dst,
-    -- this set t contains a point x
-    rcases ht.1 with ⟨x, hx⟩,
-    -- by the Hausdorff distance control, this point x is at distance at most 1
-    -- of a point y in s
-    rcases exists_edist_lt_of_Hausdorff_edist_lt hx Dst with ⟨y, hy, _⟩,
-    -- this shows that s is not empty
-    exact ⟨_, hy⟩ },
+    -- since `t` is nonempty, so is `s`
+    exact nonempty_of_Hausdorff_edist_ne_top ht.1 (ne_of_lt Dst) },
   { refine compact_iff_totally_bounded_complete.2 ⟨_, is_complete_of_is_closed s.property⟩,
     refine totally_bounded_iff.2 (λε εpos, _),
     -- we have to show that s is covered by finitely many eballs of radius ε
@@ -294,19 +278,17 @@ end
 
 /-- In a complete space, the type of nonempty compact subsets is complete. This follows
 from the same statement for closed subsets -/
-instance nonempty_compacts.complete_space [complete_space α] : complete_space (nonempty_compacts α) :=
-begin
-  apply complete_space_of_is_complete_univ,
-  apply (is_complete_image_iff nonempty_compacts.to_closeds.uniform_embedding).1,
-  apply is_complete_of_is_closed,
-  exact nonempty_compacts.is_closed_in_closeds
-end
+instance nonempty_compacts.complete_space [complete_space α] :
+  complete_space (nonempty_compacts α) :=
+(complete_space_iff_is_complete_range nonempty_compacts.to_closeds.uniform_embedding).2 $
+  is_complete_of_is_closed nonempty_compacts.is_closed_in_closeds
 
 /-- In a compact space, the type of nonempty compact subsets is compact. This follows from
 the same statement for closed subsets -/
 instance nonempty_compacts.compact_space [compact_space α] : compact_space (nonempty_compacts α) :=
 ⟨begin
   rw embedding.compact_iff_compact_image nonempty_compacts.to_closeds.uniform_embedding.embedding,
+  rw [image_univ],
   exact nonempty_compacts.is_closed_in_closeds.compact
 end⟩
 

src/topology/opens.lean

@@ -34,8 +34,8 @@ instance nonempty_compacts.to_nonempty {p : nonempty_compacts α} : nonempty p.v
 p.property.1.to_subtype
 
 /-- Associate to a nonempty compact subset the corresponding closed subset -/
-def nonempty_compacts.to_closeds [t2_space α] (s : nonempty_compacts α) : closeds α :=
-⟨s.val, closed_of_compact _ s.property.2⟩
+def nonempty_compacts.to_closeds [t2_space α] : nonempty_compacts α → closeds α :=
+set.inclusion $ λ s hs, closed_of_compact _ hs.2
 
 end nonempty_compacts
 

src/topology/uniform_space/cauchy.lean

@@ -181,7 +181,7 @@ lemma complete_univ {α : Type u} [uniform_space α] [complete_space α] :
 begin
   assume f hf _,
   rcases complete_space.complete hf with ⟨x, hx⟩,
-  exact ⟨x, by simp, hx⟩
+  exact ⟨x, mem_univ x, hx⟩
 end
 
 lemma cauchy_prod [uniform_space β] {f : filter α} {g : filter β} :
@@ -208,6 +208,10 @@ instance complete_space.prod [uniform_space β] [complete_space α] [complete_sp
 lemma complete_space_of_is_complete_univ (h : is_complete (univ : set α)) : complete_space α :=
 ⟨λ f hf, let ⟨x, _, hx⟩ := h f hf ((@principal_univ α).symm ▸ le_top) in ⟨x, hx⟩⟩
 
+lemma complete_space_iff_is_complete_univ :
+  complete_space α ↔ is_complete (univ : set α) :=
+⟨@complete_univ α _, complete_space_of_is_complete_univ⟩
+
 lemma cauchy_iff_exists_le_nhds [complete_space α] {l : filter α} (hl : l ≠ ⊥) :
   cauchy l ↔ (∃x, l ≤ 𝓝 x) :=
 ⟨complete_space.complete, assume ⟨x, hx⟩, cauchy_downwards cauchy_nhds hl hx⟩

src/topology/uniform_space/uniform_embedding.lean

@@ -33,6 +33,21 @@ lemma uniform_inducing.comp {g : β → γ} (hg : uniform_inducing g)
 structure uniform_embedding (f : α → β) extends uniform_inducing f : Prop :=
 (inj : function.injective f)
 
+lemma uniform_embedding_subtype_val {p : α → Prop} :
+  uniform_embedding (subtype.val : subtype p → α) :=
+{ comap_uniformity := rfl,
+  inj := subtype.val_injective }
+
+lemma uniform_embedding_subtype_coe {p : α → Prop} :
+  uniform_embedding (coe : subtype p → α) :=
+uniform_embedding_subtype_val
+
+lemma uniform_embedding_set_inclusion {s t : set α} (hst : s ⊆ t) :
+  uniform_embedding (inclusion hst) :=
+{ comap_uniformity :=
+    by { erw [uniformity_subtype, uniformity_subtype, comap_comap_comp], congr },
+  inj := inclusion_injective hst }
+
 lemma uniform_embedding.comp {g : β → γ} (hg : uniform_embedding g)
   {f : α → β} (hf : uniform_embedding f) : uniform_embedding (g ∘ f) :=
 { inj := function.injective_comp hg.inj hf.inj,
@@ -145,41 +160,66 @@ lemma uniform_embedding.prod {α' : Type*} {β' : Type*} [uniform_space α'] [un
 { inj := function.injective_prod h₁.inj h₂.inj,
   ..h₁.to_uniform_inducing.prod h₂.to_uniform_inducing }
 
+lemma is_complete_of_complete_image {m : α → β} {s : set α} (hm : uniform_inducing m)
+  (hs : is_complete (m '' s)) : is_complete s :=
+begin
+  intros f hf hfs,
+  rw le_principal_iff at hfs,
+  obtain ⟨_, ⟨x, hx, rfl⟩, hyf⟩ : ∃ y ∈ m '' s, map m f ≤ 𝓝 y,
+    from hs (f.map m) (cauchy_map hm.uniform_continuous hf)
+      (le_principal_iff.2 (image_mem_map hfs)),
+  rw [map_le_iff_le_comap, ← nhds_induced, ← hm.inducing.induced] at hyf,
+  exact ⟨x, hx, hyf⟩
+end
+
 /-- A set is complete iff its image under a uniform embedding is complete. -/
 lemma is_complete_image_iff {m : α → β} {s : set α} (hm : uniform_embedding m) :
   is_complete (m '' s) ↔ is_complete s :=
 begin
-  refine ⟨λ c f hf fs, _, λ c f hf fs, _⟩,
-  { let f' := map m f,
-    have cf' : cauchy f' := cauchy_map hm.to_uniform_inducing.uniform_continuous hf,
-    have f's : f' ≤ principal (m '' s),
-    { simp only [filter.le_principal_iff, set.mem_image, filter.mem_map],
-      exact mem_sets_of_superset (filter.le_principal_iff.1 fs) (λx hx, ⟨x, hx, rfl⟩) },
-    rcases c f' cf' f's with ⟨y, yms, hy⟩,
-    rcases mem_image_iff_bex.1 yms with ⟨x, xs, rfl⟩,
-    rw [map_le_iff_le_comap, ← nhds_induced, ← (uniform_embedding.embedding hm).induced] at hy,
-    exact ⟨x, xs, hy⟩ },
-  { rw filter.le_principal_iff at fs,
-    let f' := comap m f,
-    have cf' : cauchy f',
-    { have : comap m f ≠ ⊥,
-      { refine comap_ne_bot (λt ht, _),
-        have A : t ∩ m '' s ∈ f := filter.inter_mem_sets ht fs,
-        obtain ⟨x, ⟨xt, ⟨y, ys, rfl⟩⟩⟩ : (t ∩ m '' s).nonempty,
-          from nonempty_of_mem_sets hf.1 A,
-        exact ⟨y, xt⟩ },
-      apply cauchy_comap _ hf this,
-      simp only [hm.comap_uniformity, le_refl] },
-    have : f' ≤ principal s := by simp [f']; exact
-      ⟨m '' s, by simpa using fs, by simp [preimage_image_eq s hm.inj]⟩,
-    rcases c f' cf' this with ⟨x, xs, hx⟩,
-    existsi [m x, mem_image_of_mem m xs],
-    rw [(uniform_embedding.embedding hm).induced, nhds_induced] at hx,
-    calc f = map m f' : (map_comap $ filter.mem_sets_of_superset fs $ image_subset_range _ _).symm
-      ... ≤ map m (comap m (𝓝 (m x))) : map_mono hx
-      ... ≤ 𝓝 (m x) : map_comap_le }
+  refine ⟨is_complete_of_complete_image hm.to_uniform_inducing, λ c f hf fs, _⟩,
+  rw filter.le_principal_iff at fs,
+  let f' := comap m f,
+  have cf' : cauchy f',
+  { have : comap m f ≠ ⊥,
+    { refine comap_ne_bot (λt ht, _),
+      have A : t ∩ m '' s ∈ f := filter.inter_mem_sets ht fs,
+      obtain ⟨x, ⟨xt, ⟨y, ys, rfl⟩⟩⟩ : (t ∩ m '' s).nonempty,
+        from nonempty_of_mem_sets hf.1 A,
+      exact ⟨y, xt⟩ },
+    apply cauchy_comap _ hf this,
+    simp only [hm.comap_uniformity, le_refl] },
+  have : f' ≤ principal s := by simp [f']; exact
+    ⟨m '' s, by simpa using fs, by simp [preimage_image_eq s hm.inj]⟩,
+  rcases c f' cf' this with ⟨x, xs, hx⟩,
+  existsi [m x, mem_image_of_mem m xs],
+  rw [(uniform_embedding.embedding hm).induced, nhds_induced] at hx,
+  calc f = map m f' : (map_comap $ filter.mem_sets_of_superset fs $ image_subset_range _ _).symm
+    ... ≤ map m (comap m (𝓝 (m x))) : map_mono hx
+    ... ≤ 𝓝 (m x) : map_comap_le
 end
 
+lemma complete_space_iff_is_complete_range {f : α → β} (hf : uniform_embedding f) :
+  complete_space α ↔ is_complete (range f) :=
+by rw [complete_space_iff_is_complete_univ, ← is_complete_image_iff hf, image_univ]
+
+lemma complete_space_congr {e : α ≃ β} (he : uniform_embedding e) :
+  complete_space α ↔ complete_space β :=
+by rw [complete_space_iff_is_complete_range he, e.range_eq_univ,
+  complete_space_iff_is_complete_univ]
+
+lemma complete_space_coe_iff_is_complete {s : set α} :
+  complete_space s ↔ is_complete s :=
+(complete_space_iff_is_complete_range uniform_embedding_subtype_coe).trans $
+  by rw [range_coe_subtype]
+
+lemma is_complete.complete_space_coe {s : set α} (hs : is_complete s) :
+  complete_space s :=
+complete_space_coe_iff_is_complete.2 hs
+
+lemma is_closed.complete_space_coe [complete_space α] {s : set α} (hs : is_closed s) :
+  complete_space s :=
+(is_complete_of_is_closed hs).complete_space_coe
+
 lemma complete_space_extension {m : β → α} (hm : uniform_inducing m) (dense : dense_range m)
   (h : ∀f:filter β, cauchy f → ∃x:α, map m f ≤ 𝓝 x) : complete_space α :=
 ⟨assume (f : filter α), assume hf : cauchy f,