proposition: Lemma compact_impl_filter_cluster_point: forall X:TopologicalSpace, compact X -> forall F:Filter X, exists x0:X, filter_cluster_point F x0.
proof: Proof. intros. pose proof (compact_finite_nonempty_closed_intersection _ H [ G:Ensemble X | In (filter_family F) G /\ closed G ]) as [x0]. - intros. destruct H0 as [[]]; trivial. - intros. assert (closed (FamilyIntersection F')). { apply closed_family_intersection. intros. apply H1 in H2. now destruct H2, H2. } assert (In (filter_family F) (FamilyIntersection F')). { clear H2. induction H0. - rewrite empty_family_intersection. apply filter_full. - replace (FamilyIntersection (Add A x)) with (Intersection (FamilyIntersection A) x). + apply filter_intersection. * apply IHFinite. auto with sets. * assert (In (Add A x) x). { right. constructor. } apply H1 in H3. now destruct H3, H3. + extensionality_ensembles. * constructor. intros. destruct H5. ** now apply H3. ** now destruct H5. * repeat constructor; intros; apply H3; auto with sets. } apply NNPP; intro. contradiction (filter_empty _ F). replace (@Empty_set X) with (FamilyIntersection F'); trivial. extensionality_ensembles. contradiction H4. exists x. now constructor. - exists x0. red; intros. destruct H0. apply H0. constructor. split. + apply filter_upward_closed with S; trivial. apply closure_inflationary. + apply closure_closed. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)