proposition: Lemma finite_nonempty_closed_intersection_impl_compact: forall X:TopologicalSpace, (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)) -> compact X.
proof: Proof. intros. red; intros. apply NNPP; red; intro. pose (F := [ G:Ensemble X | In C (Complement G) ]). specialize (H F) as [x]. { intros. destruct H. apply H0 in H. assumption. } 2: { apply H2. assert (In (FamilyUnion C) x). { rewrite H1. constructor. } destruct H3. assert (In (Complement S) x); try contradiction. destruct H. apply H. constructor. now rewrite Complement_Complement. } intros. apply NNPP; red; intro. contradiction H2. exists [ U:Ensemble X | In F' (Complement U) ]. repeat split. - replace [U:Ensemble X | In F' (Complement U)] with (Im F' Complement). { now apply finite_image. } extensionality_ensembles. + subst. constructor. now rewrite Complement_Complement. + econstructor. * eassumption. * now rewrite Complement_Complement. - red; intros. destruct H5. apply H3 in H5. destruct H5. now rewrite Complement_Complement in H5. - extensionality_ensembles. { constructor. } apply NNPP; red; intro. contradict H4. exists x. constructor. intros. apply NNPP; red; intro. contradict H5. exists (Complement S). + constructor. rewrite Complement_Complement; trivial. + exact H6. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)