proposition: Lemma compact_cluster_set1 {T : topologicalType} (x : T) F V : hausdorff_space T -> compact V -> nbhs x V -> ProperFilter F -> F V -> cluster F = [set x] -> F --> x.
proof: Proof. move=> ? cptV nxV PF FV clFx1 U nbhsU; rewrite nbhs_simpl. wlog oU : U nbhsU / open U. rewrite /= nbhsE in nbhsU; case: nbhsU => O oO OsubU /(_ O) WH. by apply: (filterS OsubU); apply: WH; [exact: open_nbhs_nbhs | by case: oO]. have /compact_near_coveringP : compact (V `\` U). apply: (subclosed_compact _ cptV) => //. by apply: closedI; [exact: compact_closed | exact: open_closedC]. move=> /(_ _ (powerset_filter_from F) (fun W x => ~ W x))[]. move=> z [Vz ?]; have zE : x <> z by move/nbhs_singleton: nbhsU => /[swap] ->. have : ~ cluster F z by move: zE; apply: contra_not; rewrite clFx1 => ->. case/existsNP=> C /existsPNP [D] FC /existsNP [Dz] /set0P/negP/negPn/eqP. rewrite setIC => /disjoints_subset CD0; exists (D, [set W | F W /\ W `<=` C]). by split; rewrite //= nbhs_simpl; exact: powerset_filter_fromP. by case => t W [Dt] [FW] /subsetCP; apply; apply: CD0. move=> M [MF ME2 [W] MW /(_ _ MW) VUW]. apply: (@filterS _ _ _ (V `&` W)); last by apply: filterI => //; exact: MF. by move=> t [Vt Wt]; apply: contrapT => Ut; exact: (VUW t). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed