fix(topology/dense_embeddings): tweaks (#1684)

* fix(topology/dense_embeddings): tweaks

This fixes some small issues with last summer dense embedding refactors.
This is preparation for helping with Bochner integration. Some of those
fixes are backported from the perfectoid project.

* chore(dense_embedding): remove is_closed_property'

* Update src/topology/uniform_space/completion.lean

* Update src/topology/dense_embedding.lean

Author: PatrickMassot

src/topology/dense_embedding.lean

@@ -34,10 +34,13 @@ variables [topological_space β] [topological_space γ] (f : α → β) (g : β
 /-- `f : α → β` has dense range if its range (image) is a dense subset of β. -/
 def dense_range := ∀ x, x ∈ closure (range f)
 
-lemma dense_range_iff_closure_eq : dense_range f ↔ closure (range f) = univ :=
+variables {f}
+
+lemma dense_range_iff_closure_range : dense_range f ↔ closure (range f) = univ :=
 eq_univ_iff_forall.symm
 
-variables {f}
+lemma dense_range.closure_range (h : dense_range f) : closure (range f) = univ :=
+eq_univ_iff_forall.mpr h
 
 lemma dense_range.comp (hg : dense_range g) (hf : dense_range f) (cg : continuous g) :
   dense_range (g ∘ f) :=
@@ -49,7 +52,7 @@ begin
   intro c,
   rw range_comp,
   apply this,
-  rw [(dense_range_iff_closure_eq f).1 hf, image_univ],
+  rw [hf.closure_range, image_univ],
   exact hg c
 end
 
@@ -64,7 +67,7 @@ def dense_range.inhabited (df : dense_range f) (b : β) : inhabited α :=
 lemma dense_range.nonempty (hf : dense_range f) : nonempty α ↔ nonempty β :=
 ⟨nonempty.map f, λ ⟨b⟩, @nonempty_of_inhabited _ (hf.inhabited b)⟩
 
-lemma dense_range_prod {ι : Type*} {κ : Type*} {f : ι → β} {g : κ → γ}
+lemma dense_range.prod {ι : Type*} {κ : Type*} {f : ι → β} {g : κ → γ}
   (hf : dense_range f) (hg : dense_range g) : dense_range (λ p : ι × κ, (f p.1, g p.2)) :=
 have closure (range $ λ p : ι×κ, (f p.1, g p.2)) = set.prod (closure $ range f) (closure $ range g),
     by rw [←closure_prod_eq, prod_range_range_eq],
@@ -89,7 +92,7 @@ protected lemma continuous (di : dense_inducing i) : continuous i :=
 di.to_inducing.continuous
 
 lemma closure_range : closure (range i) = univ :=
-(dense_range_iff_closure_eq _).mp di.dense
+di.dense.closure_range
 
 lemma self_sub_closure_image_preimage_of_open {s : set β} (di : dense_inducing i) :
   is_open s → s ⊆ closure (i '' (i ⁻¹' s)) :=
@@ -123,7 +126,7 @@ protected lemma prod [topological_space γ] [topological_space δ]
   {e₁ : α → β} {e₂ : γ → δ} (de₁ : dense_inducing e₁) (de₂ : dense_inducing e₂) :
   dense_inducing (λ(p : α × γ), (e₁ p.1, e₂ p.2)) :=
 { induced := (de₁.to_inducing.prod_mk de₂.to_inducing).induced,
-  dense := dense_range_prod de₁.dense de₂.dense }
+  dense := de₁.dense.prod de₂.dense }
 
 variables [topological_space δ] {f : γ → α} {g : γ → δ} {h : δ → β}
 /--
@@ -263,6 +266,7 @@ protected lemma prod {e₁ : α → β} {e₂ : γ → δ} (de₁ : dense_embedd
     by simp; exact assume h₁ h₂, ⟨de₁.inj h₁, de₂.inj h₂⟩,
   ..dense_inducing.prod de₁.to_dense_inducing de₂.to_dense_inducing }
 
+/-- The dense embedding of a subtype inside its closure. -/
 def subtype_emb {α : Type*} (p : α → Prop) (e : α → β) (x : {x // p x}) :
   {x // x ∈ closure (e '' {x | p x})} :=
 ⟨e x.1, subset_closure $ mem_image_of_mem e x.2⟩
@@ -285,25 +289,39 @@ protected lemma subtype (p : α → Prop) : dense_embedding (subtype_emb p e) :=
 end dense_embedding
 
 lemma is_closed_property [topological_space β] {e : α → β} {p : β → Prop}
-  (he : closure (range e) = univ) (hp : is_closed {x | p x}) (h : ∀a, p (e a)) :
+  (he : dense_range e) (hp : is_closed {x | p x}) (h : ∀a, p (e a)) :
   ∀b, p b :=
 have univ ⊆ {b | p b},
-  from calc univ = closure (range e) : he.symm
+  from calc univ = closure (range e) : he.closure_range.symm
     ... ⊆ closure {b | p b} : closure_mono $ range_subset_iff.mpr h
     ... = _ : closure_eq_of_is_closed hp,
 assume b, this trivial
 
-lemma is_closed_property2 [topological_space α] [topological_space β] {e : α → β} {p : β → β → Prop}
-  (he : dense_embedding e) (hp : is_closed {q:β×β | p q.1 q.2}) (h : ∀a₁ a₂, p (e a₁) (e a₂)) :
+lemma is_closed_property2 [topological_space β] {e : α → β} {p : β → β → Prop}
+  (he : dense_range e) (hp : is_closed {q:β×β | p q.1 q.2}) (h : ∀a₁ a₂, p (e a₁) (e a₂)) :
   ∀b₁ b₂, p b₁ b₂ :=
 have ∀q:β×β, p q.1 q.2,
-  from is_closed_property (he.prod he).to_dense_inducing.closure_range hp $ assume a, h _ _,
+  from is_closed_property (he.prod he) hp $ λ _, h _ _,
 assume b₁ b₂, this ⟨b₁, b₂⟩
 
-lemma is_closed_property3 [topological_space α] [topological_space β] {e : α → β} {p : β → β → β → Prop}
-  (he : dense_embedding e) (hp : is_closed {q:β×β×β | p q.1 q.2.1 q.2.2}) (h : ∀a₁ a₂ a₃, p (e a₁) (e a₂) (e a₃)) :
+lemma is_closed_property3 [topological_space β] {e : α → β} {p : β → β → β → Prop}
+  (he : dense_range e) (hp : is_closed {q:β×β×β | p q.1 q.2.1 q.2.2}) (h : ∀a₁ a₂ a₃, p (e a₁) (e a₂) (e a₃)) :
   ∀b₁ b₂ b₃, p b₁ b₂ b₃ :=
 have ∀q:β×β×β, p q.1 q.2.1 q.2.2,
-  from is_closed_property (he.prod $ he.prod he).to_dense_inducing.closure_range hp $
-    assume ⟨a₁, a₂, a₃⟩, h _ _ _,
+  from is_closed_property (he.prod $ he.prod he) hp $ λ _, h _ _ _,
 assume b₁ b₂ b₃, this ⟨b₁, b₂, b₃⟩
+
+@[elab_as_eliminator]
+lemma dense_range.induction_on [topological_space β] {e : α → β} (he : dense_range e) {p : β → Prop}
+  (b₀ : β) (hp : is_closed {b | p b}) (ih : ∀a:α, p $ e a) : p b₀ :=
+is_closed_property he hp ih b₀
+
+@[elab_as_eliminator]
+lemma dense_range.induction_on₂ [topological_space β] {e : α → β} {p : β → β → Prop}
+  (he : dense_range e) (hp : is_closed {q:β×β | p q.1 q.2}) (h : ∀a₁ a₂, p (e a₁) (e a₂))
+  (b₁ b₂ : β) : p b₁ b₂ := is_closed_property2 he hp h _ _
+
+@[elab_as_eliminator]
+lemma dense_range.induction_on₃ [topological_space β] {e : α → β} {p : β → β → β → Prop}
+  (he : dense_range e) (hp : is_closed {q:β×β×β | p q.1 q.2.1 q.2.2}) (h : ∀a₁ a₂ a₃, p (e a₁) (e a₂) (e a₃))
+  (b₁ b₂ b₃ : β) : p b₁ b₂ b₃ := is_closed_property3 he hp h _ _ _

src/topology/uniform_space/abstract_completion.lean

@@ -70,7 +70,7 @@ local notation `hatα` := pkg.space
 local notation `ι` := pkg.coe
 
 lemma dense' : closure (range ι) = univ :=
-(dense_range_iff_closure_eq _).1 pkg.dense
+pkg.dense.closure_range
 
 lemma dense_inducing : dense_inducing ι :=
 ⟨pkg.uniform_inducing.inducing, pkg.dense⟩
@@ -84,7 +84,7 @@ pkg.uniform_continuous_coe.continuous
 @[elab_as_eliminator]
 lemma induction_on {p : hatα → Prop}
   (a : hatα) (hp : is_closed {a | p a}) (ih : ∀ a, p (ι a)) : p a :=
-is_closed_property pkg.dense' hp ih a
+is_closed_property pkg.dense hp ih a
 
 variables {β : Type*} [uniform_space β]
 
@@ -247,7 +247,7 @@ protected def prod : abstract_completion (α × β) :=
   complete := by apply_instance,
   separation := by apply_instance,
   uniform_inducing := uniform_inducing.prod pkg.uniform_inducing pkg'.uniform_inducing,
-  dense := dense_range_prod pkg.dense pkg'.dense }
+  dense := pkg.dense.prod pkg'.dense }
 end prod
 
 

src/topology/uniform_space/completion.lean

@@ -361,8 +361,11 @@ lemma uniform_inducing_coe : uniform_inducing  (coe : α → completion α) :=
 
 variables {α}
 
-lemma dense : closure (range (coe : α → completion α)) = univ :=
-by rw [completion.coe_eq, range_comp]; exact quotient_dense_of_dense pure_cauchy_dense
+lemma dense : dense_range (coe : α → completion α) :=
+begin
+  rw [dense_range_iff_closure_range, completion.coe_eq, range_comp],
+  exact quotient_dense_of_dense pure_cauchy_dense
+end
 
 variables (α)
 
@@ -373,7 +376,7 @@ def cpkg {α : Type*} [uniform_space α] : abstract_completion α :=
   complete := by apply_instance,
   separation := by apply_instance,
   uniform_inducing := completion.uniform_inducing_coe α,
-  dense := (dense_range_iff_closure_eq _).2 completion.dense }
+  dense := completion.dense }
 
 local attribute [instance]
 abstract_completion.uniform_struct abstract_completion.complete abstract_completion.separation
@@ -394,26 +397,19 @@ lemma uniform_embedding_coe [separated α] : uniform_embedding  (coe : α → co
 variable {α}
 
 lemma dense_inducing_coe : dense_inducing (coe : α → completion α) :=
-{ dense := (dense_range_iff_closure_eq _).2 dense,
+{ dense := dense,
   ..(uniform_inducing_coe α).inducing }
 
 lemma dense_embedding_coe [separated α]: dense_embedding (coe : α → completion α) :=
 { inj := injective_separated_pure_cauchy,
   ..dense_inducing_coe }
 
-lemma dense₂ : closure (range (λx:α × β, ((x.1 : completion α), (x.2 : completion β)))) = univ :=
-by rw [← set.prod_range_range_eq, closure_prod_eq, dense, dense, univ_prod_univ]
+lemma dense₂ : dense_range (λx:α × β, ((x.1 : completion α), (x.2 : completion β))) :=
+dense.prod dense
 
 lemma dense₃ :
-  closure (range (λx:α × (β × γ), ((x.1 : completion α), ((x.2.1 : completion β), (x.2.2 : completion γ))))) = univ :=
-let a : α → completion α := coe, bc := λp:β × γ, ((p.1 : completion β), (p.2 : completion γ)) in
-show closure (range (λx:α × (β × γ), (a x.1, bc x.2))) = univ,
-begin
-  rw [← set.prod_range_range_eq, @closure_prod_eq _ _ _ _ (range a) (range bc), ← univ_prod_univ],
-  congr,
-  exact dense,
-  exact dense₂
-end
+  dense_range (λx:α × (β × γ), ((x.1 : completion α), ((x.2.1 : completion β), (x.2.2 : completion γ)))) :=
+dense.prod dense₂
 
 @[elab_as_eliminator]
 lemma induction_on {p : completion α → Prop}
@@ -438,27 +434,6 @@ have ∀x : completion α × completion β × completion γ, p x.1 x.2.1 x.2.2,
   is_closed_property dense₃ hp $ assume ⟨a, b, c⟩, ih a b c,
 this (a, b, c)
 
-@[elab_as_eliminator]
-lemma induction_on₄ {δ : Type*} [uniform_space δ]
-  {p : completion α → completion β → completion γ → completion δ → Prop}
-  (a : completion α) (b : completion β) (c : completion γ) (d : completion δ)
-  (hp : is_closed {x : (completion α × completion β) × (completion γ × completion δ) | p x.1.1 x.1.2 x.2.1 x.2.2})
-  (ih : ∀(a:α) (b:β) (c:γ) (d : δ), p ↑a ↑b ↑c ↑d) : p a b c d :=
-let
-  ab := λp:α × β, ((p.1 : completion α), (p.2 : completion β)),
-  cd := λp:γ × δ, ((p.1 : completion γ), (p.2 : completion δ))
-in
-have dense₄ : closure (range (λx:(α × β) × (γ × δ), (ab x.1, cd x.2))) = univ,
-begin
-  rw [← set.prod_range_range_eq, @closure_prod_eq _ _ _ _ (range ab) (range cd), ← univ_prod_univ],
-  congr,
-  exact dense₂,
-  exact dense₂
-end,
-have ∀x:(completion α × completion β) × (completion γ × completion δ), p x.1.1 x.1.2 x.2.1 x.2.2, from
-  is_closed_property dense₄ hp (assume p:(α×β)×(γ×δ), ih p.1.1 p.1.2 p.2.1 p.2.2),
-this ((a, b), (c, d))
-
 lemma ext [t2_space β] {f g : completion α → β} (hf : continuous f) (hg : continuous g)
   (h : ∀a:α, f a = g a) : f = g :=
 cpkg.funext hf hg h
@@ -538,7 +513,7 @@ begin
   refine ⟨completion.extension (separation_quotient.lift (coe : α → completion α)),
     completion.map quotient.mk, _, _⟩,
   { assume a,
-    refine completion.induction_on a (is_closed_eq (continuous_map.comp continuous_extension) continuous_id) _,
+    refine induction_on a (is_closed_eq (continuous_map.comp continuous_extension) continuous_id) _,
     rintros ⟨a⟩,
     show completion.map quotient.mk (completion.extension (separation_quotient.lift coe) ↑⟦a⟧) = ↑⟦a⟧,
     rw [extension_coe (separation_quotient.uniform_continuous_lift _),