feat(Topology): codiscreteWithin = ⊥ iff IsDiscrete (#39828)

AI usage disclosure: Aristotle was used to draft the initial version, and then manually golfed.

Author: wwylele

Mathlib/Topology/DiscreteSubset.lean

@@ -365,6 +365,10 @@ lemma mem_codiscrete_subtype_iff_mem_codiscreteWithin {S : Set X} {U : Set S} :
     U ∈ codiscrete S ↔ (↑) '' U ∈ codiscreteWithin S := by
   simp [← Topology.IsEmbedding.subtypeVal.image_mem_codiscreteWithin_range]
 
+@[simp]
+theorem codiscreteWithin_eq_bot_iff {S : Set X} : codiscreteWithin S = ⊥ ↔ IsDiscrete S := by
+  simp [isDiscrete_iff_nhdsNE, codiscreteWithin, ← nhdsWithin_inter', Set.diff_eq, inter_comm]
+
 section T1Space
 
 variable [T1Space X]