proposition: Lemma separated_open_countable {R : realType} (I : Type) (B : I -> set R) (D : set I) : (forall i, open (B i)) -> (forall i, B i !=set0) -> trivIset D B -> countable D.
proof: Proof. move=> oB B0 tB; have [f fB] : {f : I -> rat & forall i, D i -> B i (ratr (f i))}. apply: (@choice _ _ (fun x y => D x -> B x (ratr y))) => i. have [r [Bir [q _ qr]]] := dense_rat (B0 _) (oB i). by exists q => Di; rewrite qr. have inj_f : {in D &, injective f}. move=> i j /[!inE] Di Dj /(congr1 ratr) ratrij. have ? : (B i `&` B j) (ratr (f i)). by split => //; [exact: fB|rewrite ratrij; exact: fB]. by apply/(tB _ _ Di Dj); exists (ratr (f i)). apply/pcard_injP; have /card_bijP/cid[g bijg] := card_rat. pose nat_of_rat (q : rat) : nat := set_val (g (to_setT q)). have inj_nat_of_rat : injective nat_of_rat. rewrite /nat_of_rat; apply: inj_comp => //; apply: inj_comp => //. exact/bij_inj. by exists (nat_of_rat \o f) => i j Di Dj /inj_nat_of_rat/inj_f; exact. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed