proposition: Lemma injective_ens_left_inverse {X Y : Type} (U : Ensemble X) (V : Ensemble Y) (f : X -> Y) (x0 : X) : In U x0 -> range f U V -> injective_ens f U -> exists g : Y -> X, range g V U /\ forall x : X, In U x -> g (f x) = x.
proof: Proof. intros Hx0 **. assert (forall y : Y, { x : X | (In (Im U f) y -> f x = y /\ In U x) /\ (~ In (Im U f) y -> x = x0) }) as ?H. { intros y. apply constructive_definite_description. destruct (classic (In (Im U f) y)). - apply Im_inv in H1. destruct H1 as [x [Hx Hxy]]. exists x. split. + split; auto. intros ?H. subst. contradict H1. exists x; auto. + intros x' []. subst. specialize (H1 (Im_def _ _ _ Hx)) as []. apply H0; auto. - exists x0. split; [split|]; auto. + intros; contradiction. + intros ? []. firstorder. } exists (fun y => proj1_sig (H1 y)). split. - intros y Hy. pose proof (proj2_sig (H1 y)) as [? ?]. destruct (classic (In (Im U f) y)); intuition. rewrite H5. assumption. - intros. pose proof (proj2_sig (H1 (f x))) as [? _]. specialize (H3 (Im_def _ _ _ H2)) as []. apply H0 in H3; auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)