proposition: Lemma surjective_ens_right_inverse {X Y : Type} (U : Ensemble X) (V : Ensemble Y) (f : X -> Y) (x0 : X) : In U x0 -> range f U V -> surjective_ens f U V -> exists g : Y -> X, range g V U /\ forall y : Y, In V y -> f (g y) = y.
proof: Proof. intros Hx0 Hf0 Hf1. destruct (choice (fun (y : Y) (x : X) => (In V y -> y = f x /\ In U x) /\ (~ In V y -> x = x0))) as [g Hg]. { intros y. destruct (classic (In V y)) as [Hy|Hy]. - destruct (Hf1 y Hy) as [x [Hx Hxy]]. subst. exists x. split; auto. intros ?. contradiction. - exists x0; split; intros; auto. contradiction. } exists g; split. - intros y Hy. specialize (Hf1 y Hy) as [x [Hx Hxy]]. subst. specialize (Hg (f x)) as [? _]. specialize (H Hy) as [_ ?]. assumption. - intros y Hy. specialize (Hg y) as [? _]. specialize (H Hy) as [? _]. congruence. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)