proposition: Lemma le_cardinal_ens_sig_injective {X Y : Type} (U : Ensemble X) (V : Ensemble Y) (f : sig U -> sig V) : injective f -> le_cardinal_ens U V.
proof: Proof. destruct (classic (inhabited Y)). 2: { left. split; auto. intros x Hx. contradict H. constructor. apply (proj1_sig (f (exist U x Hx))). } destruct H as [y0]. right. exists (sig_fn_extend (compose (@proj1_sig Y V) f) y0). split. - apply sig_fn_extend_range. intros [x Hx] _. apply (proj2_sig (f (exist U x Hx))). - apply sig_fn_extend_injective_ens. apply injective_compose; auto. intros ? ?. apply proj1_sig_injective. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)