proposition: Lemma weight_second_countable_char (X : TopologicalSpace) : second_countable X <-> (forall Y (kappa : Ensemble Y), weight X kappa -> le_cardinal_ens kappa (@Full_set nat)).
proof: Proof. split. - intros [B [HBbasis HBcount]] **. apply least_cardinal_ext_to_subset in H. destruct H as [C [[HCbasis HCmin] HCcard]]. eapply le_cardinal_ens_Proper_l; eauto. clear Y kappa HCcard. specialize (HCmin B HBbasis). apply Countable_as_le_cardinal_ens in HBcount. eapply le_cardinal_ens_transitive; eauto. - intros. destruct (weight_exists X) as [kappa [[B [HB0 HB1]]]]. red in HB0. exists B; split; auto. apply Countable_as_le_cardinal_ens. apply H. split. + exists B; split; auto. reflexivity. + intros. specialize (H0 Y V H1). clear H1. apply eq_cardinal_ens_sym in HB1. eapply le_cardinal_ens_Proper_l; eauto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)