proposition: Lemma zero_dimension_totally_disconnected {T} : zero_dimensional T -> totally_disconnected [set: T].
proof: Proof. move=> zdA x _; rewrite eqEsubset. split=> [z [R [Rx _ ctdR Rz]]|_ ->]; last exact: connected_component_refl. apply: contrapT => /eqP znx; have [U [[oU cU] Uz Ux]] := zdA _ _ znx. suff : R `&` U = R by move: Rx => /[swap] <- []. by apply: ctdR; [exists z|exists U|exists U]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed