fact: Definition surjective_ens : Prop := forall y : B, In V y -> exists x : A, In U x /\ y = f x.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)