proposition: Lemma compact_finite_nonempty_closed_intersection: forall X:TopologicalSpace, compact X -> forall F:Family X, (forall G:Ensemble X, In F G -> closed G) -> (forall F':Family X, Finite F' -> Included F' F -> Inhabited (FamilyIntersection F')) -> Inhabited (FamilyIntersection F).
proof: Proof. intros. apply NNPP; red; intro. pose (C := [ U:Ensemble X | In F (Complement U) ]). specialize (H C) as [C' [? [? ?]]]. { intros. destruct H. apply H0 in H. now apply closed_complement_open. } { extensionality_ensembles. { constructor. } apply NNPP; red; intro. contradict H2. exists x. constructor. intros. apply NNPP; red; intro. contradict H. exists (Complement S). + constructor. now rewrite Complement_Complement. + assumption. } pose (F' := [G : Ensemble X | In C' (Complement G)]). specialize (H1 F') as [x0]. { cut (F' = Im C' Complement). { intros. rewrite H1. now apply finite_image. } apply Extensionality_Ensembles; split; red; intros. - exists (Complement x). + apply H1. + now rewrite Complement_Complement. - constructor. inversion H1; subst; clear H1. now rewrite Complement_Complement. } { red; intros. destruct H1. apply H3 in H1 as []. now rewrite Complement_Complement in H1. } destruct H1. assert (In (FamilyUnion C') x). { rewrite H4. constructor. } destruct H5. assert (In (Complement S) x). { apply H1. constructor. now rewrite Complement_Complement. } contradiction H7. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)