proposition: Lemma filter_cluster_point_impl_compact: forall X:TopologicalSpace, (forall F:Filter X, exists x0:X, filter_cluster_point F x0) -> compact X.
proof: Proof. intros. apply finite_nonempty_closed_intersection_impl_compact. intros. unshelve refine (let H2:=_ in let filt := Build_Filter_from_subbasis F H2 in _). - intros. rewrite indexed_to_family_intersection. apply H1. + apply FiniteT_img; trivial. intros. apply classic. + red; intros. destruct H4. rewrite H5; apply H3. - assert (filter_subbasis filt F) by apply filter_from_subbasis_subbasis. destruct (H filt) as [x0]. exists x0. constructor; intros. assert (closed S) by now apply H0. assert (In (filter_family filt) S). { eapply filter_subbasis_elements; eassumption. } pose proof (H4 _ H7). now rewrite closure_fixes_closed in H8. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)