proposition: Lemma inverse_map_ens_range_bijective_ens {A B : Type} (f : A -> B) (g : B -> A) (U : Ensemble A) (V : Ensemble B) : range f U V -> inverse_map_ens f g U V -> bijective_ens g V U.
proof: Proof. intros Hf_range Hfg. destruct Hfg as [Hgf Hfg]. split. - intros b0 b1 Hb0 Hb1 Hb. rewrite <- (Hfg b0 Hb0), <- (Hfg b1 Hb1). congruence. - intros a Ha. exists (f a). split; auto. symmetry; auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)