proposition: Lemma le_cardinal_ens_Im {X Y : Type} (f : X -> Y) (U : Ensemble X) : le_cardinal_ens (Im U f) U.
proof: Proof. destruct (classic (Inhabited U)). 2: { destruct (classic (inhabited X)). - destruct H0 as [x0]. right. exists (fun _ => x0). split; intros ? **. + contradict H. inversion H0; subst; clear H0. firstorder. + contradict H. inversion H0; subst; clear H0. firstorder. - left; split; [firstorder|]. intros y Hy. inversion Hy; subst; clear Hy. apply H; exists x. assumption. } destruct H as [x0 Hx0]. pose proof (surjective_ens_right_inverse U (Im U f) f x0 Hx0) as [g [Hg0 Hg1]]. { apply range_char_Im. reflexivity. } { apply surjective_ens_Im. } right. exists g; split; auto. intros y0 y1 Hy0 Hy1. pose proof (Hg1 y0 Hy0). pose proof (Hg1 y1 Hy1). congruence. 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)