proposition: Lemma clopen_countable {T : topologicalType}: compact [set: T] -> @second_countable T -> countable (@clopen T).
proof: Proof. move=> cmpT [B /fset_subset_countable cntB] [obase Bbase]. apply/(card_le_trans _ cntB)/pcard_surjP. pose f := fun F : {fset set T} => \bigcup_(x in [set` F]) x; exists f. move=> D [] oD cD /=; have cmpt : cover_compact D. by rewrite -compact_cover; exact: (subclosed_compact _ cmpT). have h (x : T) : exists V : set T, D x -> [/\ B V, nbhs x V & V `<=` D]. have [Dx|] := pselect (D x); last by move=> ?; exists set0. have [V [BV Vx VD]] := Bbase x D (open_nbhs_nbhs (conj oD Dx)). exists V => _; split => //; apply: open_nbhs_nbhs; split => //. exact: obase. pose h' := fun z => projT1 (cid (h z)). have [fs fsD DsubC] : finite_subset_cover D h' D. apply: cmpt. - by move=> z Dz; apply: obase; have [] := projT2 (cid (h z)) Dz. - move=> z Dz; exists z => //; apply: nbhs_singleton. by have [] := projT2 (cid (h z)) Dz. exists [fset h' z | z in fs]%fset. move=> U/imfsetP [z /=] /fsD /set_mem Dz ->; rewrite inE. by have [] := projT2 (cid (h z)) Dz. rewrite eqEsubset; split => z. case=> y /imfsetP [x /= /fsD/set_mem Dx ->]; move: z. by have [] := projT2 (cid (h x)) Dx. move=> /DsubC /= [y /= yfs hyz]; exists (h' y) => //. by rewrite set_imfset /=; exists y. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed