proposition: Lemma closed_compact: forall (X:TopologicalSpace) (S:Ensemble X), compact X -> closed S -> compact (SubspaceTopology S).
proof: Proof. intros. apply net_cluster_point_impl_compact. intros. destruct (compact_impl_net_cluster_point _ H _ (fun i:DS_set I => subspace_inc _ (x i))) as [x0]; trivial. assert (In S x0). { rewrite <- (closure_fixes_closed S); trivial. eapply net_cluster_point_in_closure; [ | eassumption ]. destruct H1 as [i0]. exists i0. intros. now destruct (x j). } exists (exist _ x0 H3). red; intros. red; intros. rewrite subspace_open_char in H4. destruct H4 as [V []]. rewrite H6 in H5. destruct H5. simpl in H5. destruct (H2 V H4 H5 i) as [j []]; trivial. exists j; split; trivial. rewrite H6. now constructor. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)