proposition: Lemma bijective_impl_invertible_ens_dec {A B : Type} (f : A -> B) (U : Ensemble A) (V : Ensemble B) (a0 : A) (HV : forall b : B, In V b \/ ~ In V b) : range f U V -> bijective_ens f U V -> exists g : B -> A, inverse_map_ens f g U V.
proof: Proof. intros Hf [Hf0 Hf1]. assert (forall b : B, { a : A | (In V b -> In U a /\ f a = b) /\ (~ In V b -> a = a0) }). { intros b. apply constructive_definite_description. specialize (HV b) as [Hb|Hb]. - specialize (Hf1 b Hb) as [a [Ha0 Ha1]]. subst. exists a. split; firstorder. - exists a0. split; firstorder. } exists (fun b => proj1_sig (X b)). split. - intros a Ha. pose proof (proj2_sig (X (f a))) as [Ha0 _]. specialize (Ha0 (Hf a Ha)) as [Ha0 Ha1]. apply Hf0 in Ha1; auto. - intros b Hb. pose proof (proj2_sig (X b)) as [Hb0 _]. specialize (Hb0 Hb) as [_ Hb1]. assumption. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)