proposition: Lemma ultrafilter_limit_impl_compact: forall X:TopologicalSpace, (forall U:Filter X, ultrafilter U -> exists x0:X, filter_limit U x0) -> compact X.
proof: Proof. intros. apply filter_cluster_point_impl_compact. intros. destruct (ultrafilter_extension F) as [U]. destruct H0. destruct (H _ H1) as [x0]. exists x0. red; intros. apply filter_limit_is_cluster_point in H2. apply H0 in H3. now apply H2. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)