proposition: Lemma net_cluster_point_impl_compact: forall X:TopologicalSpace, (forall (I:DirectedSet) (x:Net I X), inhabited (DS_set I) -> exists x0:X, net_cluster_point x x0) -> compact X.
proof: Proof. intros. apply filter_cluster_point_impl_compact. intros. destruct (H _ (filter_to_net _ F)) as [x0]. - cut (inhabited X). + intro. destruct H0 as [x]. exists. simpl. apply Build_filter_to_net_DS_set with Full_set x. * apply filter_full. * constructor. + apply NNPP; intro. contradiction (filter_empty _ F). replace (@Empty_set X) with (@Full_set X). * apply filter_full. * extensionality_ensembles. contradiction H0. now constructor. - exists x0. now apply filter_to_net_cluster_point_impl_filter_cluster_point. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)