proposition: Theorem Lindelof_Lemma (X : TopologicalSpace) {Y0 Y1 : Type} (kappa : Ensemble Y0) (lambda : Ensemble Y1) : Lindelof_degree X kappa -> weight X lambda -> le_cardinal_ens kappa lambda.
proof: Proof. intros [?Hkappa0 ?Hkappa0]. intros H. apply least_cardinal_ext_to_subset in H. destruct H as [B [[?HB0 ?HB0] ?Hlambda]]. eapply le_cardinal_ens_Proper_r; eauto. clear Y1 lambda Hlambda. apply Hkappa1. clear Y0 kappa Hkappa0 Hkappa1. apply Lindelof_Lemma_technical'; auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)