proposition: Lemma bijective_ens_impl_invertible_ens {A B : Type} (f : A -> B) (U : Ensemble A) (V : Ensemble B) (a0 : A) : range f U V -> bijective_ens f U V -> exists g : B -> A, inverse_map_ens f g U V.
proof: Proof. apply bijective_impl_invertible_ens_dec; auto. intros ?. apply classic. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)