proposition: Lemma injective_finite_inverse_image_Singleton {X Y : Type} (f : X -> Y) (y : Y) : injective f -> Finite (inverse_image f (Singleton y)).
proof: Proof. intros Hf. destruct (classic (exists x : X, f x = y)) as [H|H]. - destruct H as [x Hx]. subst. rewrite (proj1 (injective_inverse_image_Singleton f) Hf x). apply Singleton_is_finite. - replace (inverse_image _ _) with (@Empty_set X). { constructor. } apply Extensionality_Ensembles; split. { intros ? ?; contradiction. } intros x Hx. destruct Hx. contradict H. exists x. destruct H0. reflexivity. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)