proposition: Lemma Lindelof_degree_candidate_upwards_closed (X : TopologicalSpace) : forall {Y0 Y1 : Type} (kappa : Ensemble Y0) (lambda : Ensemble Y1), Lindelof_degree_candidate X kappa -> le_cardinal_ens kappa lambda -> Lindelof_degree_candidate X lambda.
proof: Proof. intros. red. intros. specialize (H cover H1). destruct H as [scover []]. exists scover. split; try assumption. eapply le_cardinal_ens_transitive; eauto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)