proposition: Corollary subspace_weight_le_space {Y0 Y1 : Type} (kappa : Ensemble Y0) (lambda : Ensemble Y1) : weight X kappa -> weight SubspaceTopology lambda -> le_cardinal_ens lambda kappa.
proof: Proof. intros HX HS. destruct HX as [[BX [HBX0 HBX1]] HBX2]. destruct HS as [[BS [HBS0 HBS1]] HBS2]. apply le_cardinal_ens_transitive with (V := (Im BX (inverse_image subspace_inc))). - apply HBS2. eexists; split. 2: reflexivity. apply subspace_basis. assumption. - eapply le_cardinal_ens_Proper_r; eauto. apply le_cardinal_ens_Im. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)