refactor(topology/separation): rename indistinguishable to inseparable (#14401)

* Replace `indistinguishable` by `inseparable` in the definition and lemma names. The word "indistinguishable" is too generic.
* Rename `t0_space_iff_distinguishable` to `t0_space_iff_not_inseparable` because the name `t0_space_iff_separable` is misleading, slightly golf the proof.
* Add `t0_space_iff_nhds_injective`, `nhds_injective`, reorder lemmas around these two.

Author: urkud

src/algebraic_geometry/properties.lean

@@ -31,15 +31,15 @@ variable (X : Scheme)
 
 instance : t0_space X.carrier :=
 begin
-  rw t0_space_iff_distinguishable,
+  rw t0_space_iff_not_inseparable,
   intros x y h h',
   obtain ⟨U, R, ⟨e⟩⟩ := X.local_affine x,
   have hy := (h' _ U.1.2).mp U.2,
-  erw ← subtype_indistinguishable_iff (⟨x, U.2⟩ : U.1.1) (⟨y, hy⟩ : U.1.1) at h',
+  erw ← subtype_inseparable_iff (⟨x, U.2⟩ : U.1.1) (⟨y, hy⟩ : U.1.1) at h',
   let e' : U.1 ≃ₜ prime_spectrum R :=
     homeo_of_iso ((LocallyRingedSpace.forget_to_SheafedSpace ⋙ SheafedSpace.forget _).map_iso e),
   have := t0_space_of_injective_of_continuous e'.injective e'.continuous,
-  rw t0_space_iff_distinguishable at this,
+  rw t0_space_iff_not_inseparable at this,
   exact this ⟨x, U.2⟩ ⟨y, hy⟩ (by simpa using h) h'
 end
 

src/topology/maps.lean

@@ -17,7 +17,7 @@ This file introduces the following properties of a map `f : X → Y` between top
 
 * `inducing f` means the topology on `X` is the one induced via `f` from the topology on `Y`.
   These behave like embeddings except they need not be injective. Instead, points of `X` which
-  are identified by `f` are also indistinguishable in the topology on `X`.
+  are identified by `f` are also inseparable in the topology on `X`.
 * `embedding f` means `f` is inducing and also injective. Equivalently, `f` identifies `X` with
   a subspace of `Y`.
 * `open_embedding f` means `f` is an embedding with open image, so it identifies `X` with an

src/topology/metric_space/basic.lean

@@ -1022,8 +1022,8 @@ by { convert metric.emetric_closed_ball ε.2, simp }
 @[simp] lemma metric.emetric_ball_top (x : α) : emetric.ball x ⊤ = univ :=
 eq_univ_of_forall $ λ y, edist_lt_top _ _
 
-lemma metric.indistinguishable_iff {x y : α} : indistinguishable x y ↔ dist x y = 0 :=
-by rw [emetric.indistinguishable_iff, edist_nndist, dist_nndist, ennreal.coe_eq_zero,
+lemma metric.inseparable_iff {x y : α} : inseparable x y ↔ dist x y = 0 :=
+by rw [emetric.inseparable_iff, edist_nndist, dist_nndist, ennreal.coe_eq_zero,
   nnreal.coe_eq_zero]
 
 /-- Build a new pseudometric space from an old one where the bundled uniform structure is provably
@@ -2514,7 +2514,7 @@ separated_def.2 $ λ x y h, eq_of_forall_dist_le $
 /-- If a `pseudo_metric_space` is a T₀ space, then it is a `metric_space`. -/
 def of_t0_pseudo_metric_space (α : Type*) [pseudo_metric_space α] [t0_space α] :
   metric_space α :=
-{ eq_of_dist_eq_zero := λ x y hdist, indistinguishable.eq $ metric.indistinguishable_iff.2 hdist,
+{ eq_of_dist_eq_zero := λ x y hdist, inseparable.eq $ metric.inseparable_iff.2 hdist,
   ..‹pseudo_metric_space α› }
 
 /-- A metric space induces an emetric space -/

src/topology/metric_space/emetric_space.lean

@@ -613,8 +613,8 @@ theorem tendsto_at_top [nonempty β] [semilattice_sup β] {u : β → α} {a : 
 (at_top_basis.tendsto_iff nhds_basis_eball).trans $
   by simp only [exists_prop, true_and, mem_Ici, mem_ball]
 
-theorem indistinguishable_iff : indistinguishable x y ↔ edist x y = 0 :=
-by simp [indistinguishable_iff_closure, mem_closure_iff, edist_comm, forall_lt_iff_le']
+theorem inseparable_iff : inseparable x y ↔ edist x y = 0 :=
+by simp [inseparable_iff_closure, mem_closure_iff, edist_comm, forall_lt_iff_le']
 
 /-- In a pseudoemetric space, Cauchy sequences are characterized by the fact that, eventually,
 the pseudoedistance between its elements is arbitrarily small -/
@@ -890,7 +890,7 @@ separated_def.2 $ λ x y h, eq_of_forall_edist_le $
 /-- If a `pseudo_emetric_space` is a T₀ space, then it is an `emetric_space`. -/
 def emetric.of_t0_pseudo_emetric_space (α : Type*) [pseudo_emetric_space α] [t0_space α] :
   emetric_space α :=
-{ eq_of_edist_eq_zero := λ x y hdist, indistinguishable.eq $ emetric.indistinguishable_iff.2 hdist,
+{ eq_of_edist_eq_zero := λ x y hdist, inseparable.eq $ emetric.inseparable_iff.2 hdist,
   ..‹pseudo_emetric_space α› }
 
 /-- Auxiliary function to replace the uniformity on an emetric space with

src/topology/separation.lean

@@ -88,7 +88,7 @@ If the space is also compact:
 https://en.wikipedia.org/wiki/Separation_axiom
 -/
 
-open set filter topological_space
+open function set filter topological_space
 open_locale topological_space filter classical
 
 universes u v
@@ -166,58 +166,59 @@ lemma t0_space_def (α : Type u) [topological_space α] :
   t0_space α ↔ ∀ x y, x ≠ y → ∃ U:set α, is_open U ∧ (xor (x ∈ U) (y ∈ U)) :=
 by { split, apply @t0_space.t0, apply t0_space.mk }
 
-/-- Two points are topologically indistinguishable if no open set separates them. -/
-def indistinguishable {α : Type u} [topological_space α] (x y : α) : Prop :=
+/-- Two points are topologically inseparable if no open set separates them. -/
+def inseparable {α : Type u} [topological_space α] (x y : α) : Prop :=
 ∀ (U : set α) (hU : is_open U), x ∈ U ↔ y ∈ U
 
-lemma indistinguishable_iff_nhds_eq {x y : α} : indistinguishable x y ↔ 𝓝 x = 𝓝 y :=
+lemma inseparable_iff_nhds_eq {x y : α} : inseparable x y ↔ 𝓝 x = 𝓝 y :=
 ⟨λ h, by simp only [nhds_def', h _] { contextual := tt },
   λ h U hU, by simp only [← hU.mem_nhds_iff, h]⟩
 
-alias indistinguishable_iff_nhds_eq ↔ indistinguishable.nhds_eq _
+alias inseparable_iff_nhds_eq ↔ inseparable.nhds_eq _
 
-lemma indistinguishable.map [topological_space β] {x y : α} {f : α → β}
-  (h : indistinguishable x y) (hf : continuous f) :
-  indistinguishable (f x) (f y) :=
+lemma inseparable.map [topological_space β] {x y : α} {f : α → β}
+  (h : inseparable x y) (hf : continuous f) :
+  inseparable (f x) (f y) :=
 λ U hU, h (f ⁻¹' U) (hU.preimage hf)
 
-lemma t0_space_iff_distinguishable (α : Type u) [topological_space α] :
-  t0_space α ↔ ∀ (x y : α), x ≠ y → ¬ indistinguishable x y :=
-begin
-  delta indistinguishable,
-  rw t0_space_def,
-  push_neg,
-  simp_rw xor_iff_not_iff,
-end
+lemma t0_space_iff_not_inseparable (α : Type u) [topological_space α] :
+  t0_space α ↔ ∀ (x y : α), x ≠ y → ¬inseparable x y :=
+by simp only [t0_space_def, xor_iff_not_iff, not_forall, exists_prop, inseparable]
 
-lemma t0_space_iff_indistinguishable (α : Type u) [topological_space α] :
-  t0_space α ↔ ∀ (x y : α), indistinguishable x y → x = y :=
-(t0_space_iff_distinguishable α).trans $ forall₂_congr $ λ a b, not_imp_not
+lemma t0_space_iff_inseparable (α : Type u) [topological_space α] :
+  t0_space α ↔ ∀ (x y : α), inseparable x y → x = y :=
+by simp only [t0_space_iff_not_inseparable, ne.def, not_imp_not]
 
-@[simp] lemma nhds_eq_nhds_iff [t0_space α] {a b : α} : 𝓝 a = 𝓝 b ↔ a = b :=
-function.injective.eq_iff $ λ x y h, of_not_not $
-  λ hne, (t0_space_iff_distinguishable α).mp ‹_› x y hne (indistinguishable_iff_nhds_eq.mpr h)
+lemma inseparable.eq [t0_space α] {x y : α} (h : inseparable x y) : x = y :=
+(t0_space_iff_inseparable α).1 ‹_› x y h
 
-lemma indistinguishable.eq [t0_space α] {x y : α} (h : indistinguishable x y) : x = y :=
-nhds_eq_nhds_iff.mp h.nhds_eq
+lemma t0_space_iff_nhds_injective (α : Type u) [topological_space α] :
+  t0_space α ↔ injective (𝓝 : α → filter α) :=
+by simp only [t0_space_iff_inseparable, injective, inseparable_iff_nhds_eq]
+
+lemma nhds_injective [t0_space α] : injective (𝓝 : α → filter α) :=
+(t0_space_iff_nhds_injective α).1 ‹_›
+
+@[simp] lemma nhds_eq_nhds_iff [t0_space α] {a b : α} : 𝓝 a = 𝓝 b ↔ a = b :=
+nhds_injective.eq_iff
 
-lemma indistinguishable_iff_closed {x y : α} :
-  indistinguishable x y ↔ ∀ (U : set α) (hU : is_closed U), x ∈ U ↔ y ∈ U :=
+lemma inseparable_iff_closed {x y : α} :
+  inseparable x y ↔ ∀ (U : set α) (hU : is_closed U), x ∈ U ↔ y ∈ U :=
 ⟨λ h U hU, not_iff_not.mp (h _ hU.1), λ h U hU, not_iff_not.mp (h _ (is_closed_compl_iff.mpr hU))⟩
 
-lemma indistinguishable_iff_closure (x y : α) :
-  indistinguishable x y ↔ x ∈ closure ({y} : set α) ∧ y ∈ closure ({x} : set α) :=
+lemma inseparable_iff_closure (x y : α) :
+  inseparable x y ↔ x ∈ closure ({y} : set α) ∧ y ∈ closure ({x} : set α) :=
 begin
-  rw indistinguishable_iff_closed,
+  rw inseparable_iff_closed,
   exact ⟨λ h, ⟨(h _ is_closed_closure).mpr (subset_closure $ set.mem_singleton y),
       (h _ is_closed_closure).mp (subset_closure $ set.mem_singleton x)⟩,
     λ h U hU, ⟨λ hx, (is_closed.closure_subset_iff hU).mpr (set.singleton_subset_iff.mpr hx) h.2,
       λ hy, (is_closed.closure_subset_iff hU).mpr (set.singleton_subset_iff.mpr hy) h.1⟩⟩
 end
 
-lemma subtype_indistinguishable_iff {α : Type u} [topological_space α] {U : set α} (x y : U) :
-  indistinguishable x y ↔ indistinguishable (x : α) y :=
-by { simp_rw [indistinguishable_iff_closure, closure_subtype, image_singleton] }
+lemma subtype_inseparable_iff {α : Type u} [topological_space α] {U : set α} (x y : U) :
+  inseparable x y ↔ inseparable (x : α) y :=
+by { simp_rw [inseparable_iff_closure, closure_subtype, image_singleton] }
 
 theorem minimal_nonempty_closed_subsingleton [t0_space α] {s : set α} (hs : is_closed s)
   (hmin : ∀ t ⊆ s, t.nonempty → is_closed t → t = s) :
@@ -298,15 +299,15 @@ embedding_subtype_coe.t0_space
 
 theorem t0_space_iff_or_not_mem_closure (α : Type u) [topological_space α] :
   t0_space α ↔ (∀ a b : α, a ≠ b → (a ∉ closure ({b} : set α) ∨ b ∉ closure ({a} : set α))) :=
-by simp only [t0_space_iff_distinguishable, indistinguishable_iff_closure, not_and_distrib]
+by simp only [t0_space_iff_not_inseparable, inseparable_iff_closure, not_and_distrib]
 
 instance [topological_space β] [t0_space α] [t0_space β] : t0_space (α × β) :=
-(t0_space_iff_indistinguishable _).2 $
+(t0_space_iff_inseparable _).2 $
   λ x y h, prod.ext (h.map continuous_fst).eq (h.map continuous_snd).eq
 
 instance {ι : Type*} {π : ι → Type*} [Π i, topological_space (π i)] [Π i, t0_space (π i)] :
   t0_space (Π i, π i) :=
-(t0_space_iff_indistinguishable _).2 $ λ x y h, funext $ λ i, (h.map (continuous_apply i)).eq
+(t0_space_iff_inseparable _).2 $ λ x y h, funext $ λ i, (h.map (continuous_apply i)).eq
 
 /-- A T₁ space, also known as a Fréchet space, is a topological space
   where every singleton set is closed. Equivalently, for every pair

src/topology/sets/opens.lean

@@ -199,7 +199,7 @@ protected lemma comap_comap (g : C(β, γ)) (f : C(α, β)) (U : opens γ) :
   comap f (comap g U) = comap (g.comp f) U := rfl
 
 lemma comap_injective [t0_space β] : injective (comap : C(α, β) → frame_hom (opens β) (opens α)) :=
-λ f g h, continuous_map.ext $ λ a, indistinguishable.eq $ λ s hs, begin
+λ f g h, continuous_map.ext $ λ a, inseparable.eq $ λ s hs, begin
   simp_rw ←mem_preimage,
   congr' 2,
   have := fun_like.congr_fun h ⟨_, hs⟩,

src/topology/sober.lean

@@ -66,12 +66,12 @@ begin
     λ h U hU, not_imp_not.mp (h _ (is_open_compl_iff.mpr hU))⟩,
 end
 
-lemma indistinguishable_iff_specializes_and (x y : α) :
-  indistinguishable x y ↔ x ⤳ y ∧ y ⤳ x :=
-(indistinguishable_iff_closure x y).trans (and_comm _ _)
+lemma inseparable_iff_specializes_and (x y : α) :
+  inseparable x y ↔ x ⤳ y ∧ y ⤳ x :=
+(inseparable_iff_closure x y).trans (and_comm _ _)
 
 lemma specializes_antisymm [t0_space α] (x y : α) : x ⤳ y → y ⤳ x → x = y :=
-λ h₁ h₂, ((indistinguishable_iff_specializes_and _ _).mpr ⟨h₁, h₂⟩).eq
+λ h₁ h₂, ((inseparable_iff_specializes_and _ _).mpr ⟨h₁, h₂⟩).eq
 
 lemma specializes.map {x y : α} (h : x ⤳ y) {f : α → β} (hf : continuous f) : f x ⤳ f y :=
 begin