feat: strengthen instTotallyDisconnectedSpaceOfIsUltrametricDist to…

… `TotallySeparatedSpace` (#17427)

Rename the file it's in to `TotallySeparated`. Also add two lemmas `isClopen_of_disjoint_cover_open` and `totallySeparatedSpace_iff_exists_isClopen`.

Mathlib.lean

@@ -4744,7 +4744,7 @@ import Mathlib.Topology.MetricSpace.ThickenedIndicator
 import Mathlib.Topology.MetricSpace.Thickening
 import Mathlib.Topology.MetricSpace.Ultra.Basic
 import Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
-import Mathlib.Topology.MetricSpace.Ultra.TotallyDisconnected
+import Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
 import Mathlib.Topology.Metrizable.Basic
 import Mathlib.Topology.Metrizable.ContinuousMap
 import Mathlib.Topology.Metrizable.Uniformity

Mathlib/Topology/Clopen.lean

@@ -102,6 +102,10 @@ theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s)
   rintro x ⟨hx₁, hx₂⟩
   exact ⟨hx₁, by simpa [not_mem_of_mem_compl hx₂] using cover hx₁⟩
 
+theorem isClopen_of_disjoint_cover_open {a b : Set X} (cover : univ ⊆ a ∪ b)
+    (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen a :=
+  univ_inter a ▸ isClopen_inter_of_disjoint_cover_clopen isClopen_univ cover ha hb hab
+
 @[simp]
 theorem isClopen_discrete [DiscreteTopology X] (s : Set X) : IsClopen s :=
   ⟨isClosed_discrete _, isOpen_discrete _⟩

Mathlib/Topology/Connected/TotallyDisconnected.lean

@@ -195,7 +195,7 @@ alias IsTotallySeparated.isTotallyDisconnected := isTotallyDisconnected_of_isTot
 
 /-- A space is totally separated if any two points can be separated by two disjoint open sets
 covering the whole space. -/
-class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where
+@[mk_iff] class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where
   /-- The universal set `Set.univ` in a totally separated space is totally separated. -/
   isTotallySeparated_univ : IsTotallySeparated (univ : Set α)
 
@@ -210,15 +210,19 @@ instance (priority := 100) TotallySeparatedSpace.of_discrete (α : Type*) [Topol
   ⟨fun _ _ b _ h => ⟨{b}ᶜ, {b}, isOpen_discrete _, isOpen_discrete _, h, rfl,
     (compl_union_self _).symm.subset, disjoint_compl_left⟩⟩
 
+theorem totallySeparatedSpace_iff_exists_isClopen {α : Type*} [TopologicalSpace α] :
+    TotallySeparatedSpace α ↔ ∀ x y : α, x ≠ y → ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ := by
+  simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]
+  refine forall₃_congr fun x y _ ↦
+    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩
+  · exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
+      Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩
+  · exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩
+
 theorem exists_isClopen_of_totally_separated {α : Type*} [TopologicalSpace α]
     [TotallySeparatedSpace α] {x y : α} (hxy : x ≠ y) :
-    ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ := by
-  obtain ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ :=
-    TotallySeparatedSpace.isTotallySeparated_univ (Set.mem_univ x) (Set.mem_univ y) hxy
-  have hU := isClopen_inter_of_disjoint_cover_clopen isClopen_univ f hU hV disj
-  rw [univ_inter _] at hU
-  rw [← Set.subset_compl_iff_disjoint_right, subset_compl_comm] at disj
-  exact ⟨U, hU, Ux, disj Vy⟩
+    ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ :=
+  totallySeparatedSpace_iff_exists_isClopen.mp ‹_› _ _ hxy
 
 end TotallySeparated
 
@@ -260,7 +264,6 @@ theorem Continuous.connectedComponentsLift_unique (h : Continuous f) (g : Connec
     (hg : g ∘ (↑) = f) : g = h.connectedComponentsLift :=
   connectedComponents_lift_unique' <| hg.trans h.connectedComponentsLift_comp_coe.symm
 
-
 instance ConnectedComponents.totallyDisconnectedSpace :
     TotallyDisconnectedSpace (ConnectedComponents α) := by
   rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]

Mathlib/Topology/MetricSpace/Ultra/TotallySeparated.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky, David Loeffler
+-/
+import Mathlib.Topology.MetricSpace.Defs
+import Mathlib.Topology.MetricSpace.Ultra.Basic
+
+/-!
+# Ultrametric spaces are totally separated
+
+In a metric space with an ultrametric, the space is totally separated, hence totally disconnected.
+
+## Tags
+
+ultrametric, nonarchimedean, totally separated, totally disconnected
+-/
+open Metric IsUltrametricDist
+
+instance {X : Type*} [MetricSpace X] [IsUltrametricDist X] : TotallySeparatedSpace X :=
+  totallySeparatedSpace_iff_exists_isClopen.mpr fun x y h ↦ by
+    obtain ⟨r, hr, hr'⟩ := exists_between (dist_pos.mpr h)
+    refine ⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩
+    · simp only [mem_ball, dist_self, hr]
+    · simp only [Set.mem_compl, mem_ball, dist_comm, not_lt, hr'.le]
+
+example {X : Type*} [MetricSpace X] [IsUltrametricDist X] : TotallyDisconnectedSpace X :=
+  inferInstance