proposition: Lemma closed_compact_ens (X : TopologicalSpace) (S : Ensemble X) : compact X -> closed S -> forall F : Family X, (forall U, In F U -> open U) -> Included S (FamilyUnion F) -> exists C, Finite C /\ Included C F /\ Included S (FamilyUnion C).
proof: Proof. intros X_compact S_closed cover_of_S cover_open cover_covers. specialize (X_compact (Union cover_of_S (Singleton (Complement S)))) as [fincover [Hfincover0 [Hfincover1 Hfincover2]]]. { intros. destruct H; auto. destruct H. auto. } { rewrite family_union_union. rewrite family_union_singleton. apply union_complement_included_l. assumption. } exists (Intersection cover_of_S fincover); repeat split. - apply Intersection_preserves_finite. assumption. - intros U HU. apply Intersection_decreases_l in HU. assumption. - intros x Hx. assert (In (FamilyUnion fincover) x). { rewrite Hfincover2. constructor. } destruct H. exists S0; auto. split; auto. apply Hfincover1 in H. destruct H. 2: { destruct H; contradiction. } assumption. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)