proposition: Lemma bijective_ens_compose (f : A -> B) (g : B -> C) : range f U V -> bijective_ens f U V -> bijective_ens g V W -> bijective_ens (compose g f) U W.
proof: Proof. intros Hf [Hf0 Hf1] [Hg0 Hg1]. split. - eapply injective_ens_compose; eauto. - eapply surjective_ens_compose; eauto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)