From 6f6502b0f8cdf0f7cc4d72b443119046611bf6eb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 17 May 2026 16:25:33 +0900 Subject: [PATCH] make discrete_topology a ptopologicalType Co-authored-by: @agontard Co-authored-by: Cyril Cohen --- theories/topology_theory/discrete_topology.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v index 0e681b3ce6..72bd27fbdc 100644 --- a/theories/topology_theory/discrete_topology.v +++ b/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) :=