refactor(topology/uniform_space/separated): drop is_separated (#16458)

This predicate is no longer used outside of this file. If we'll need it in the future, then we can redefine it for any topological space in terms of `inseparable`.

Also rename `topology.uniform_space.compact_separated` to `topology.uniform_space.compact`.

src/analysis/box_integral/basic.lean

@@ -5,7 +5,7 @@ Authors: Yury Kudryashov
 -/
 import analysis.box_integral.partition.filter
 import analysis.box_integral.partition.measure
-import topology.uniform_space.compact_separated
+import topology.uniform_space.compact
 
 /-!
 # Integrals of Riemann, Henstock-Kurzweil, and McShane

src/topology/algebra/uniform_group.lean

@@ -6,7 +6,7 @@ Authors: Patrick Massot, Johannes Hölzl
 import topology.uniform_space.uniform_convergence
 import topology.uniform_space.uniform_embedding
 import topology.uniform_space.complete_separated
-import topology.uniform_space.compact_separated
+import topology.uniform_space.compact
 import topology.algebra.group
 import tactic.abel
 

src/topology/continuous_function/compact.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import topology.continuous_function.bounded
-import topology.uniform_space.compact_separated
+import topology.uniform_space.compact
 import topology.compact_open
 import topology.sets.compacts
 

src/topology/uniform_space/separation.lean

@@ -37,7 +37,6 @@ is equivalent to asking that the uniform structure induced on `s` is separated.
 
 * `separation_relation X : set (X × X)`: the separation relation
 * `separated_space X`: a predicate class asserting that `X` is separated
-* `is_separated s`: a predicate asserting that `s : set X` is separated
 * `separation_quotient X`: the maximal separated quotient of `X`.
 * `separation_quotient.lift f`: factors a map `f : X → Y` through the separation quotient of `X`.
 * `separation_quotient.map f`: turns a map `f : X → Y` into a map between the separation quotients
@@ -136,6 +135,11 @@ lemma eq_of_forall_symmetric {α : Type*} [uniform_space α] [separated_space α
   (h : ∀ {V}, V ∈ 𝓤 α → symmetric_rel V → (x, y) ∈ V) : x = y :=
 eq_of_uniformity_basis has_basis_symmetric (by simpa [and_imp] using λ _, h)
 
+lemma eq_of_cluster_pt_uniformity [separated_space α] {x y : α} (h : cluster_pt (x, y) (𝓤 α)) :
+  x = y :=
+eq_of_uniformity_basis uniformity_has_basis_closed $ λ V ⟨hV, hVc⟩,
+  is_closed_iff_cluster_pt.1 hVc _ $ h.mono $ le_principal_iff.2 hV
+
 lemma id_rel_sub_separation_relation (α : Type*) [uniform_space α] : id_rel ⊆ 𝓢 α :=
 begin
   unfold separation_rel,
@@ -235,86 +239,6 @@ lemma is_closed_range_of_spaced_out {ι} [separated_space α] {V₀ : set (α ×
 is_closed_of_spaced_out V₀_in $
   by { rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ h, exact hf x y (ne_of_apply_ne f h) }
 
-/-!
-### Separated sets
--/
-
-/-- A set `s` in a uniform space `α` is separated if the separation relation `𝓢 α`
-induces the trivial relation on `s`. -/
-def is_separated (s : set α) : Prop := ∀ x y ∈ s, (x, y) ∈ 𝓢 α → x = y
-
-lemma is_separated_def (s : set α) : is_separated s ↔ ∀ x y ∈ s, (x, y) ∈ 𝓢 α → x = y :=
-iff.rfl
-
-lemma is_separated_def' (s : set α) : is_separated s ↔ (s ×ˢ s) ∩ 𝓢 α ⊆ id_rel :=
-begin
-  rw is_separated_def,
-  split,
-  { rintros h ⟨x, y⟩ ⟨⟨x_in, y_in⟩, H⟩,
-    simp [h x x_in y y_in H] },
-  { intros h x x_in y y_in xy_in,
-    rw ← mem_id_rel,
-    exact h ⟨mk_mem_prod x_in y_in, xy_in⟩ }
-end
-
-lemma is_separated.mono {s t : set α} (hs : is_separated s) (hts : t ⊆ s) : is_separated t :=
-λ x hx y hy, hs x (hts hx) y (hts hy)
-
-lemma univ_separated_iff : is_separated (univ : set α) ↔ separated_space α :=
-begin
-  simp only [is_separated, mem_univ, true_implies_iff, separated_space_iff],
-  split,
-  { intro h,
-    exact subset.antisymm (λ ⟨x, y⟩ xy_in, h x y xy_in) (id_rel_sub_separation_relation α), },
-  { intros h x y xy_in,
-    rwa h at xy_in },
-end
-
-lemma is_separated_of_separated_space [separated_space α] (s : set α) : is_separated s :=
-begin
-  rw [is_separated, separated_space.out],
-  tauto,
-end
-
-lemma is_separated_iff_induced {s : set α} : is_separated s ↔ separated_space s :=
-begin
-  rw separated_space_iff,
-  change _ ↔ 𝓢 {x // x ∈ s} = _,
-  rw [separation_rel_comap rfl, is_separated_def'],
-  split; intro h,
-  { ext ⟨⟨x, x_in⟩, ⟨y, y_in⟩⟩,
-    suffices : (x, y) ∈ 𝓢 α ↔ x = y, by simpa only [mem_id_rel],
-    refine ⟨λ H, h ⟨mk_mem_prod x_in y_in, H⟩, _⟩,
-    rintro rfl,
-    exact id_rel_sub_separation_relation α rfl },
-  { rintros ⟨x, y⟩ ⟨⟨x_in, y_in⟩, hS⟩,
-    have A : (⟨⟨x, x_in⟩, ⟨y, y_in⟩⟩ : ↥s × ↥s) ∈ prod.map (coe : s → α) (coe : s → α) ⁻¹' 𝓢 α,
-      from hS,
-    simpa using h.subset A }
-end
-
-lemma eq_of_uniformity_inf_nhds_of_is_separated {s : set α} (hs : is_separated s) :
-  ∀ {x y : α}, x ∈ s → y ∈ s → cluster_pt (x, y) (𝓤 α) → x = y :=
-begin
-  intros x y x_in y_in H,
-  have : ∀ V ∈ 𝓤 α, (x, y) ∈ closure V,
-  { intros V V_in,
-    rw mem_closure_iff_cluster_pt,
-    have : 𝓤 α ≤ 𝓟 V, by rwa le_principal_iff,
-    exact H.mono this },
-  apply hs x x_in y y_in,
-  simpa [separation_rel_eq_inter_closure],
-end
-
-lemma eq_of_uniformity_inf_nhds [separated_space α] :
-  ∀ {x y : α}, cluster_pt (x, y) (𝓤 α) → x = y :=
-begin
-  have : is_separated (univ : set α),
-  { rw univ_separated_iff,
-    assumption },
-  introv,
-  simpa using eq_of_uniformity_inf_nhds_of_is_separated this,
-end
 
 /-!
 ### Separation quotient
@@ -440,11 +364,6 @@ lemma eq_of_separated_of_uniform_continuous [separated_space β] {f : α → β}
   (H : uniform_continuous f) (h : x ≈ y) : f x = f y :=
 separated_def.1 (by apply_instance) _ _ $ separated_of_uniform_continuous H h
 
-lemma _root_.is_separated.eq_of_uniform_continuous {f : α → β} {x y : α} {s : set β}
-  (hs : is_separated s) (hxs : f x ∈ s) (hys : f y ∈ s) (H : uniform_continuous f) (h : x ≈ y) :
-  f x = f y :=
-(is_separated_def _).mp hs _ hxs _ hys $ λ _ h', h _ (H h')
-
 /-- The maximal separated quotient of a uniform space `α`. -/
 def separation_quotient (α : Type*) [uniform_space α] := quotient (separation_setoid α)
 
@@ -519,10 +438,4 @@ separated_def.2 $ assume x y H, prod.ext
   (eq_of_separated_of_uniform_continuous uniform_continuous_fst H)
   (eq_of_separated_of_uniform_continuous uniform_continuous_snd H)
 
-lemma _root_.is_separated.prod {s : set α} {t : set β} (hs : is_separated s) (ht : is_separated t) :
-  is_separated (s ×ˢ t) :=
-(is_separated_def _).mpr $ λ x hx y hy H, prod.ext
-  (hs.eq_of_uniform_continuous hx.1 hy.1 uniform_continuous_fst H)
-  (ht.eq_of_uniform_continuous hx.2 hy.2 uniform_continuous_snd H)
-
 end uniform_space