proposition: Lemma Lindelof_Lemma_technical: forall (X:TopologicalSpace) (B:Family X), open_basis B -> forall C:Family X, open_cover C -> exists V:Family X, subcover V C /\ le_cardinal_ens V B.
proof: Proof. intros. pose (basis_elts_contained_in_cover_elt := [ U:Ensemble X | In B U /\ Inhabited U /\ exists V:Ensemble X, In C V /\ Included U V ]). destruct (choice (fun (U:{U | In basis_elts_contained_in_cover_elt U}) (V:Ensemble X) => In C V /\ Included (proj1_sig U) V)) as [choice_fun Hcf]. { intros. destruct x. simpl. now destruct i as [[? [? ?]]]. } exists (Im Full_set choice_fun). repeat split. - red; intros. destruct_ensembles_in. subst. apply Hcf. - intros x Hx. destruct Hx. destruct (open_basis_cover B H x S) as [V [? []]]; trivial. { now apply H0. } unshelve eexists (choice_fun (exist _ V _)). { constructor. repeat split; trivial. - now exists x. - exists S; now split. } + apply Im_def. constructor. + apply Hcf. simpl. assumption. - eapply le_cardinal_ens_transitive. { apply le_cardinal_ens_Im. } eapply le_cardinal_ens_Proper_l. { apply eq_cardinal_ens_sym. apply eq_cardinal_ens_sig. } apply le_cardinal_ens_Included. firstorder. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)