proposition: Lemma separated_closed_ball_countable {R : realType} (I : Type) (B : I -> set R) (D : set I) : (forall i, (radius (B i))%:num > 0) -> trivIset D (fun i => closed_ball (cpoint (B i)) (radius (B i))%:num) -> countable D.
proof: Proof. move=> B0 tD. have : trivIset D (fun i => ball (cpoint (B i)) (radius (B i))%:num). move=> i j Di Dj BiBj; apply: tD => //. by apply: subsetI_neq0 BiBj => //; exact: subset_closed_ball. apply: separated_open_countable => //; first by move=> i; exact: ball_open. by move=> i; eexists; exact: ballxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule