proposition: Lemma eq_cardinal_ens_Im_injective {X Y : Type} (U : Ensemble X) (f : X -> Y) : injective_ens f U -> eq_cardinal_ens U (Im U f).
proof: Proof. intros Hf. right. exists f. split. - apply range_char_Im. reflexivity. - split. + assumption. + apply surjective_ens_Im. 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)