From 5800b553368828c2664d7de4dff2006ce44de351 Mon Sep 17 00:00:00 2001 From: zstone1 Date: Thu, 29 Jun 2023 10:37:54 -0400 Subject: [PATCH] Update theories/cantor.v Co-authored-by: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> --- theories/cantor.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/cantor.v b/theories/cantor.v index be0284c5cf..0378a4bd91 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -35,7 +35,7 @@ Definition cantor_like (T : topologicalType) := hausdorff_space T & zero_dimensional T]. -Canonical cantor_psuedoMetric {R} := +Canonical cantor_pseudoMetric {R} := @product_pseudoMetricType R _ (fun (_ : nat) => @discrete_pseudoMetricType R _ discrete_bool) (countableP _).