proposition: Lemma inverse_image_injective_cardinal_le {X Y : Type} (f : X -> Y) (U : Ensemble Y) : injective f -> le_cardinal_ens (inverse_image f U) U.
proof: Proof. intros Hf. right. exists f. split. - apply range_char_inverse_image. reflexivity. - apply injective_injective_ens, Hf. 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)