proposition: Lemma clopen_surj {R : realType} {T : pseudoMetricType R} : compact [set: T] -> $|{surjfun [set: nat] >-> @clopen T}|.
proof: Proof. move=> cmptT. suff : @clopen T = set0 \/ $|{surjfun [set: nat] >-> @clopen T}|. by case => //; rewrite eqEsubset => -[/(_ _ clopenT)]. exact/pfcard_geP/clopen_countable/compact_second_countable. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed