proposition: Lemma sig_fn_extend_surjective_ens {X Y : Type} {P : X -> Prop} (f : sig P -> Y) (y0 : Y) (V : Ensemble Y) : surjective_ens (sig_fn_extend f y0) P V <-> surjective_ens f Full_set V.
proof: Proof. split. - intros Hf y Hy. specialize (Hf y Hy) as [x [Hx Hxy]]. subst. exists (exist P x Hx). split; [constructor|]. cbv. destruct (classic_dec _); try contradiction. destruct (proof_irrelevance _ Hx p); reflexivity. - intros Hf y Hy. specialize (Hf y Hy) as [[x Hx] [_ Hxy]]. subst. exists x. split; auto. cbv. destruct (classic_dec _); try contradiction. destruct (proof_irrelevance _ Hx p); reflexivity. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)