feat(uniform_space/separation): add separated_set (#3130)

Also add documentation and simplify the proof of separated => t2 and add the converse. 



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

Author: PatrickMassot

src/topology/algebra/group_completion.lean

@@ -65,7 +65,7 @@ instance is_add_group_hom_coe : is_add_group_hom (coe : α → completion α) :=
 
 variables {β : Type v} [uniform_space β] [add_group β] [uniform_add_group β]
 
-lemma is_add_group_hom_extension  [complete_space β] [separated β]
+lemma is_add_group_hom_extension  [complete_space β] [separated_space β]
   {f : α → β} [is_add_group_hom f] (hf : continuous f) : is_add_group_hom (completion.extension f) :=
 have hf : uniform_continuous f, from uniform_continuous_of_continuous hf,
 { map_add := assume a b, completion.induction_on₂ a b

src/topology/algebra/uniform_group.lean

@@ -339,7 +339,7 @@ variables [topological_space α] [add_comm_group α] [topological_add_group α]
 variables [topological_space β] [add_comm_group β] [topological_add_group β]
 variables [topological_space γ] [add_comm_group γ] [topological_add_group γ]
 variables [topological_space δ] [add_comm_group δ] [topological_add_group δ]
-variables [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated G] [complete_space G]
+variables [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated_space G] [complete_space G]
 variables {e : β → α} [is_add_group_hom e] (de : dense_inducing e)
 variables {f : δ → γ} [is_add_group_hom f] (df : dense_inducing f)
 variables {φ : β × δ → G} (hφ : continuous φ) [bilin : is_Z_bilin φ]

src/topology/algebra/uniform_ring.lean

@@ -97,7 +97,7 @@ variables {β : Type u} [uniform_space β] [ring β] [uniform_add_group β] [top
           (f : α →+* β) (hf : continuous f)
 
 /-- The completion extension as a ring morphism. -/
-def extension_hom [complete_space β] [separated β] :
+def extension_hom [complete_space β] [separated_space β] :
   completion α →+* β :=
 have hf : uniform_continuous f, from uniform_continuous_of_continuous hf,
 { to_fun := completion.extension f,

src/topology/category/UniformSpace.lean

@@ -58,7 +58,7 @@ structure CpltSepUniformSpace :=
 (α : Type u)
 [is_uniform_space : uniform_space α]
 [is_complete_space : complete_space α]
-[is_separated : separated α]
+[is_separated : separated_space α]
 
 namespace CpltSepUniformSpace
 
@@ -71,10 +71,10 @@ def to_UniformSpace (X : CpltSepUniformSpace) : UniformSpace :=
 UniformSpace.of X
 
 instance (X : CpltSepUniformSpace) : complete_space ((to_UniformSpace X).α) := CpltSepUniformSpace.is_complete_space X
-instance (X : CpltSepUniformSpace) : separated ((to_UniformSpace X).α) := CpltSepUniformSpace.is_separated X
+instance (X : CpltSepUniformSpace) : separated_space ((to_UniformSpace X).α) := CpltSepUniformSpace.is_separated X
 
 /-- Construct a bundled `UniformSpace` from the underlying type and the appropriate typeclasses. -/
-def of (X : Type u) [uniform_space X] [complete_space X] [separated X] : CpltSepUniformSpace := ⟨X⟩
+def of (X : Type u) [uniform_space X] [complete_space X] [separated_space X] : CpltSepUniformSpace := ⟨X⟩
 
 /-- The category instance on `CpltSepUniformSpace`. -/
 instance category : category CpltSepUniformSpace :=
@@ -136,7 +136,7 @@ adjunction.mk_of_hom_equiv
     right_inv := λ f,
     begin
       apply subtype.eq, funext x, cases f,
-      exact @completion.extension_coe _ _ _ _ _ (CpltSepUniformSpace.separated _) f_property _
+      exact @completion.extension_coe _ _ _ _ _ (CpltSepUniformSpace.separated_space _) f_property _
     end },
   hom_equiv_naturality_left_symm' := λ X X' Y f g,
   begin

src/topology/metric_space/basic.lean

@@ -651,7 +651,7 @@ end metric
 open metric
 
 @[priority 100] -- see Note [lower instance priority]
-instance metric_space.to_separated : separated α :=
+instance metric_space.to_separated : separated_space α :=
 separated_def.2 $ λ x y h, eq_of_forall_dist_le $
   λ ε ε0, le_of_lt (h _ (dist_mem_uniformity ε0))
 

src/topology/metric_space/completion.lean

@@ -142,7 +142,7 @@ protected lemma completion.eq_of_dist_eq_zero (x y : completion α) (h : dist x
 begin
   /- This follows from the separation of `completion α` and from the description of
   entourages in terms of the distance. -/
-  have : separated (completion α) := by apply_instance,
+  have : separated_space (completion α) := by apply_instance,
   refine separated_def.1 this x y (λs hs, _),
   rcases (completion.mem_uniformity_dist s).1 hs with ⟨ε, εpos, hε⟩,
   rw ← h at εpos,

src/topology/metric_space/emetric_space.lean

@@ -375,7 +375,7 @@ open emetric
 
 /-- An emetric space is separated -/
 @[priority 100] -- see Note [lower instance priority]
-instance to_separated : separated α :=
+instance to_separated : separated_space α :=
 separated_def.2 $ λ x y h, eq_of_forall_edist_le $
 λ ε ε0, le_of_lt (h _ (edist_mem_uniformity ε0))
 

src/topology/separation.lean

@@ -122,6 +122,40 @@ t2_iff_nhds.trans
      let ⟨f, hf, uf⟩ := exists_ultrafilter xy in
      h f uf (le_trans hf inf_le_left) (le_trans hf inf_le_right)⟩
 
+lemma is_closed_diagonal [t2_space α] : is_closed (diagonal α) :=
+is_closed_iff_nhds.mpr $ assume ⟨a₁, a₂⟩ h, eq_of_nhds_ne_bot $ assume : 𝓝 a₁ ⊓ 𝓝 a₂ = ⊥, h $
+  let ⟨t₁, ht₁, t₂, ht₂, (h' : t₁ ∩ t₂ ⊆ ∅)⟩ :=
+    by rw [←empty_in_sets_eq_bot, mem_inf_sets] at this; exact this in
+  begin
+    change t₁ ∈ 𝓝 a₁ at ht₁,
+    change t₂ ∈ 𝓝 a₂ at ht₂,
+    rw [nhds_prod_eq, ←empty_in_sets_eq_bot],
+    apply filter.sets_of_superset,
+    apply inter_mem_inf_sets (prod_mem_prod ht₁ ht₂) (mem_principal_sets.mpr (subset.refl _)),
+    exact assume ⟨x₁, x₂⟩ ⟨⟨hx₁, hx₂⟩, (heq : x₁ = x₂)⟩,
+      show false, from @h' x₁ ⟨hx₁, heq.symm ▸ hx₂⟩
+  end
+
+lemma t2_iff_is_closed_diagonal : t2_space α ↔ is_closed (diagonal α) :=
+begin
+  split,
+  { introI h,
+    exact is_closed_diagonal },
+  { intro h,
+    constructor,
+    intros x y hxy,
+    have : (x, y) ∈ -diagonal α, by rwa [mem_compl_iff],
+    obtain ⟨t, t_sub, t_op, xyt⟩ : ∃ t ⊆ -diagonal α, is_open t ∧ (x, y) ∈ t :=
+      is_open_iff_forall_mem_open.mp h _ this,
+    rcases is_open_prod_iff.mp t_op x y xyt with ⟨U, V, U_op, V_op, xU, yV, H⟩,
+    use [U, V, U_op, V_op, xU, yV],
+    have := subset.trans H t_sub,
+    rw eq_empty_iff_forall_not_mem,
+    rintros z ⟨zU, zV⟩,
+    have : ¬ (z, z) ∈ diagonal α := this (mk_mem_prod zU zV),
+    exact this rfl },
+end
+
 @[simp] lemma nhds_eq_nhds_iff {a b : α} [t2_space α] : 𝓝 a = 𝓝 b ↔ a = b :=
 ⟨assume h, eq_of_nhds_ne_bot $ by rw [h, inf_idem]; exact nhds_ne_bot, assume h, h ▸ rfl⟩
 
@@ -202,20 +236,6 @@ instance Pi.t2_space {α : Type*} {β : α → Type v} [t₂ : Πa, topological_
   let ⟨i, hi⟩ := not_forall.mp (mt funext h) in
   separated_by_f (λz, z i) (infi_le _ i) hi⟩
 
-lemma is_closed_diagonal [t2_space α] : is_closed {p:α×α | p.1 = p.2} :=
-is_closed_iff_nhds.mpr $ assume ⟨a₁, a₂⟩ h, eq_of_nhds_ne_bot $ assume : 𝓝 a₁ ⊓ 𝓝 a₂ = ⊥, h $
-  let ⟨t₁, ht₁, t₂, ht₂, (h' : t₁ ∩ t₂ ⊆ ∅)⟩ :=
-    by rw [←empty_in_sets_eq_bot, mem_inf_sets] at this; exact this in
-  begin
-    change t₁ ∈ 𝓝 a₁ at ht₁,
-    change t₂ ∈ 𝓝 a₂ at ht₂,
-    rw [nhds_prod_eq, ←empty_in_sets_eq_bot],
-    apply filter.sets_of_superset,
-    apply inter_mem_inf_sets (prod_mem_prod ht₁ ht₂) (mem_principal_sets.mpr (subset.refl _)),
-    exact assume ⟨x₁, x₂⟩ ⟨⟨hx₁, hx₂⟩, (heq : x₁ = x₂)⟩,
-      show false, from @h' x₁ ⟨hx₁, heq.symm ▸ hx₂⟩
-  end
-
 variables [topological_space β]
 
 lemma is_closed_eq [t2_space α] {f g : β → α}

src/topology/uniform_space/abstract_completion.lean

@@ -55,7 +55,7 @@ structure abstract_completion (α : Type u) [uniform_space α] :=
 (coe : α → space)
 (uniform_struct : uniform_space space)
 (complete : complete_space space)
-(separation : separated space)
+(separation : separated_space space)
 (uniform_inducing : uniform_inducing coe)
 (dense : dense_range coe)
 
@@ -110,7 +110,7 @@ begin
   exact pkg.dense_inducing.extend_eq_of_cont hf.continuous a
 end
 
-variables [complete_space β] [separated β]
+variables [complete_space β] [separated_space β]
 
 lemma uniform_continuous_extend : uniform_continuous (pkg.extend f) :=
 begin
@@ -178,7 +178,7 @@ pkg.map_unique pkg uniform_continuous_id (assume a, rfl)
 
 variables {γ : Type*} [uniform_space γ]
 
-lemma extend_map [complete_space γ] [separated γ] {f : β → γ} {g : α → β}
+lemma extend_map [complete_space γ] [separated_space γ] {f : β → γ} {g : α → β}
   (hf : uniform_continuous f) (hg : uniform_continuous g) :
   pkg'.extend f ∘ map g = pkg.extend (f ∘ g) :=
 pkg.funext (pkg'.continuous_extend.comp (pkg.continuous_map pkg' _)) pkg.continuous_extend $ λ a,
@@ -263,7 +263,7 @@ open function
 protected def extend₂ (f : α → β → γ) : hatα → hatβ → γ :=
 curry $ (pkg.prod pkg').extend (uncurry f)
 
-variables [separated γ] {f : α → β → γ}
+variables [separated_space γ] {f : α → β → γ}
 
 lemma extension₂_coe_coe (hf : uniform_continuous $ uncurry f) (a : α) (b : β) :
   pkg.extend₂ pkg' f (ι a) (ι' b) = f a b :=

src/topology/uniform_space/complete_separated.lean

@@ -17,7 +17,7 @@ open_locale topological_space
 variables {α : Type*}
 
 /-In a separated space, a complete set is closed -/
-lemma is_closed_of_is_complete  [uniform_space α] [separated α] {s : set α} (h : is_complete s) :
+lemma is_closed_of_is_complete  [uniform_space α] [separated_space α] {s : set α} (h : is_complete s) :
   is_closed s :=
 is_closed_iff_nhds.2 $ λ a ha, begin
   let f := 𝓝 a ⊓ principal s,
@@ -29,7 +29,7 @@ end
 namespace dense_inducing
 open filter
 variables [topological_space α] {β : Type*} [topological_space β]
-variables {γ : Type*} [uniform_space γ] [complete_space γ] [separated γ]
+variables {γ : Type*} [uniform_space γ] [complete_space γ] [separated_space γ]
 
 lemma continuous_extend_of_cauchy {e : α → β} {f : α → γ}
   (de : dense_inducing e) (h : ∀ b : β, cauchy (map f (comap e $ 𝓝 b))) :