proposition: Lemma compactness_on_indexed_covers: forall (X:TopologicalSpace) (A:Type) (C:IndexedFamily A X), compact X -> (forall a:A, open (C a)) -> IndexedUnion C = Full_set -> exists A':Ensemble A, Finite A' /\ IndexedUnion (fun a':{a':A | In A' a'} => C (proj1_sig a')) = Full_set.
proof: Proof. intros. pose (cover := ImageFamily C). destruct (H cover) as [subcover]. { intros. destruct H2. rewrite H3; apply H0. } { unfold cover. now rewrite <- indexed_to_family_union. } destruct H2 as [? []]. destruct (finite_choice _ _ (fun (U:{U:Ensemble X | In subcover U}) (a:A) => proj1_sig U = C a)) as [choice_fun]. { now apply Finite_ens_type. } { destruct x as [U]. simpl. apply H3 in i. destruct i. now exists x. } exists (Im Full_set choice_fun). split. - apply FiniteT_img. + now apply Finite_ens_type. + intros; apply classic. - extensionality_ensembles. { constructor. } assert (In Full_set x) by constructor. rewrite <- H4 in H6. destruct H6. assert (In (Im Full_set choice_fun) (choice_fun (exist _ S H6))). { exists (exist _ S H6); constructor. } exists (exist _ (choice_fun (exist _ S H6)) H8). simpl. now rewrite <- H5. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)