proposition: Lemma cluster_cvgE F : Filter F -> cluster F = [set p | exists2 G, ProperFilter G & G --> p /\ F `<=` G].
proof: Proof. move=> FF; have [F0|nF0] := pselect (F set0). have -> : cluster F = set0. by rewrite -subset0 clusterE => x /(_ set0 F0); rewrite closure0. by apply/esym; rewrite -subset0 => p [? PG [_ /(_ set0 F0)]]; apply PG. rewrite predeqE => p; have PF : ProperFilter F by []. split=> [clFp|[G Gproper [cvGp sFG]] A B]; last first. by move=> /sFG GA /cvGp GB; apply: (@filter_ex _ G); apply: filterI. exists (filter_from (\bigcup_(A in F) [set A `&` B | B in nbhs p]) id). apply: filter_from_proper; last first. by move=> _ [A FA [B p_B <-]]; have := clFp _ _ FA p_B. apply: filter_from_filter. exists setT; exists setT; first exact: filterT. by exists setT; [apply: filterT|rewrite setIT]. move=> _ _ [A1 FA1 [B1 p_B1 <-]] [A2 FA2 [B2 p_B2 <-]]. exists (A1 `&` B1 `&` (A2 `&` B2)) => //; exists (A1 `&` A2). exact: filterI. by exists (B1 `&` B2); [apply: filterI|rewrite setIACA]. split. move=> A p_A; exists A => //; exists setT; first exact: filterT. by exists A => //; rewrite setIC setIT. move=> A FA; exists A => //; exists A => //; exists setT; first exact: filterT. by rewrite setIT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed