extra application of discrete_topology

math-comp · Oct 3, 2024 · 1724e44 · 1724e44
1 parent 9bc5555
commit 1724e44
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/cantor.v b/theories/cantor.v
@@ -484,7 +484,7 @@ Local Lemma cantor_surj_pt1 : exists2 f : Tree -> T,
 Proof.
 pose entn n := projT2 (cid (ent_balls' (count_unif n))).
 have [ | |? []//| |? []// | |] := @tree_map_props
-    (discrete_topology \o K) T (embed_refine) (embed_invar) cptT hsdfT.
+    K T (embed_refine) (embed_invar) cptT hsdfT.
 - move=> n U; rewrite eqEsubset; split=> [t Ut|t [? ? []]//].
   have [//|_ _ _ + _] := entn n; rewrite -subTset.
   move=> /(_ t I)[W cbW Wt]; exists (existT _ W cbW) => //.