proposition: Lemma compact_ultra (T : topologicalType) : compact = [set A | forall F : set_system T, UltraFilter F -> F A -> A `&` [set p | F --> p] !=set0].
proof: Proof. rewrite predeqE => A; split=> Aco F FF FA. by have /Aco [p [?]] := FA; rewrite ultra_cvg_clusterE; exists p. have [G [GU sFG]] := ultraFilterLemma FF. have /Aco [p [Ap]] : G A by apply: sFG. rewrite /= -[_ --> p]/([set _ | _] p) -ultra_cvg_clusterE. by move=> /(cvg_cluster sFG); exists p. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed