fact: Definition sig_fn_extend {X Y : Type} {P : X -> Prop} (f : sig P -> Y) (y : Y) : X -> Y := sig_fn_extend_dec (fun x => classic_dec (P x)) f y.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)