feat: prove T597, hyperconnected with an isolated point gives a generic point

PiBaseLean.lean

@@ -934,6 +934,7 @@ import PiBaseLean.Theorems.T587.Theorem
 import PiBaseLean.Theorems.T59.Theorem
 import PiBaseLean.Theorems.T590.Theorem
 import PiBaseLean.Theorems.T594.Theorem
+import PiBaseLean.Theorems.T597.Theorem
 import PiBaseLean.Theorems.T60.Theorem
 import PiBaseLean.Theorems.T61.Theorem
 import PiBaseLean.Theorems.T610.Theorem

PiBaseLean/Theorems/T597/Theorem.lean

@@ -0,0 +1,38 @@
+module
+
+public import PiBaseLean.Bundled.Basic
+public import PiBaseLean.Properties.P39.Bundled
+public import PiBaseLean.Properties.P139.Bundled
+public import PiBaseLean.Properties.P201.Bundled
+
+@[expose] public section
+
+universe u
+
+open Set
+
+namespace PiBase
+
+variable {X : Type u} [TopologicalSpace X]
+
+/-- Theorem T597: P39 ⊓ P139 ≤ P201
+
+If `p` is isolated then `{p}` is nonempty open, so hyperconnectedness makes every nonempty
+open set meet `{p}` — that is, contain `p`. Hence every neighbourhood of every point meets
+`{p}`, so `closure {p}` is everything. -/
+theorem instHasGenericPointOfPreirreducibleSpaceOfHasAnIsolatedPoint
+    [hp : PreirreducibleSpace X] [hi : HasAnIsolatedPoint X] : HasGenericPoint X := by
+  obtain ⟨p, hop⟩ := hi.ex_isolated
+  refine ⟨p, ?_⟩
+  refine Set.eq_univ_of_forall fun x ↦ mem_closure_iff.2 fun U hU hxU ↦ ?_
+  obtain ⟨z, _, hz⟩ := hp.isPreirreducible_univ {p} U hop hU ⟨p, trivial, rfl⟩ ⟨x, trivial, hxU⟩
+  exact ⟨z, hz.2, hz.1⟩
+
+end PiBase
+
+namespace PiBase.Formal
+
+theorem T597 : P39 ⊓ P139 ≤ P201 := fun X _ ⟨h1, h2⟩ ↦
+  @instHasGenericPointOfPreirreducibleSpaceOfHasAnIsolatedPoint X _ h1 h2
+
+end PiBase.Formal