Merge pull request #1975 from affeldt-aist/discrete_topology_20260517

make discrete_topology a ptopologicalType

Author: CohenCyril

theories/topology_theory/discrete_topology.v

@@ -189,6 +189,7 @@ HB.instance Definition _ (T : choiceType) :=
   hasNbhs.Build (discrete_topology T) principal_filter.
 HB.instance Definition _ (T : choiceType) :=
   Discrete_ofNbhs.Build (discrete_topology T) erefl.
+HB.saturate discrete_topology.
 HB.instance Definition _ (T : choiceType) :=
   DiscreteUniform_ofNbhs.Build (discrete_topology T).
 HB.instance Definition _ {R : numDomainType} (T : choiceType) :=