proposition: Corollary injective_finite_inverse_image {X Y : Type} (f : X -> Y) (U : Ensemble Y) : injective f -> Finite U -> Finite (inverse_image f U).
proof: Proof. intros Hf HU. apply Finite_as_lt_cardinal_ens. apply Finite_as_lt_cardinal_ens in HU. apply (inverse_image_injective_cardinal_le f U) in Hf. eapply le_lt_cardinal_ens_transitive; eauto. 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)