proposition: Lemma compact_closed: forall (X:TopologicalSpace) (S:Ensemble X), Hausdorff X -> compact (SubspaceTopology S) -> closed S.
proof: Proof. intros. destruct (classic (Inhabited S)). 2: { red. rewrite (not_inhabited_empty _ H1). rewrite Complement_Empty_set. apply open_full. } replace S with (closure S). { apply closure_closed. } apply Extensionality_Ensembles; split; red; intros. 2: { apply closure_inflationary. assumption. } destruct (net_limits_determine_topology _ _ H2) as [I0 [y []]]. pose (yS (i:DS_set I0) := exist (fun x:X => In S x) (y i) (H3 i)). assert (inhabited (SubspaceTopology S)). { destruct H1. constructor. now exists x0. } assert (inhabited (DS_set I0)) as HinhI0. { red in H4. destruct (H4 Full_set) as [i0]; auto with topology. constructor. } pose proof (compact_impl_net_cluster_point (SubspaceTopology S) H0 _ yS HinhI0). destruct H6 as [[x0]]. apply net_cluster_point_impl_subnet_converges in H6. 2: { destruct (H4 Full_set). - apply open_full. - constructor. - now constructor. } destruct H6 as [J [y' []]]. destruct H6. assert (net_limit (fun j:DS_set J => y (h j)) x0). { apply continuous_func_preserves_net_limits with (f:=subspace_inc S) (Y:=X) in H7. - assumption. - apply continuous_func_continuous_everywhere, subspace_inc_continuous. } assert (net_limit (fun j:DS_set J => y (h j)) x). { apply subnet_limit with I0 y; trivial. now constructor. } assert (x = x0). { eapply Hausdorff_impl_net_limit_unique; eassumption. } now subst. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)