proposition: Lemma totally_disconnected_cvg {T : topologicalType} (x : T) : hausdorff_space T -> zero_dimensional T -> compact [set: T] -> filter_from [set D : set T | D x /\ clopen D] id --> x.
proof: Proof. pose F := filter_from [set D : set T | D x /\ clopen D] id. have FF : Filter F. apply: filter_from_filter; first by exists setT; split => //; exact: clopenT. by move=> A B [? ?] [? ?]; exists (A `&` B) => //; split=> //; exact: clopenI. have PF : ProperFilter F by apply: filter_from_proper; move=> ? [? _]; exists x. move=> hsdfT zdT cmpT U Ux; rewrite nbhs_simpl -/F. wlog oU : U Ux / open U. move: Ux; rewrite /= nbhsE => -[] V [? ?] /filterS + /(_ V) P. by apply; apply: P => //; exists V. have /(iffLR (compact_near_coveringP _)) : compact (~` U). by apply: (subclosed_compact _ cmpT) => //; exact: open_closedC. move=> /(_ _ _ setC (powerset_filter_from_filter PF))[]. move=> y nUy; have /zdT [C [[oC cC] Cx Cy]] : x != y. by apply: contra_notN nUy => /eqP <-; exact: nbhs_singleton. exists (~` C, [set U | U `<=` C]); first split. - by apply: open_nbhs_nbhs; split => //; exact: closed_openC. - apply/near_powerset_filter_fromP; first by move=> ? ?; exact: subset_trans. by exists C => //; exists C. - by case=> i j [? /subsetC]; apply. by move=> D [DF _ [C DC]]/(_ _ DC)/subsetC2/filterS; apply; exact: DF. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed