[Coq-Club] Pointwise definition of function

[Anton Podkopaev]

Hello,

I'm trying to define a function pointwise. To do so, I'd like to prove the
following lemma:

Definition pointwise_func_def {A B} (P : B -> Prop)
(H : forall (n : A), exists fn, P fn) :
exists (f : A -> B), forall n, P (f n).

I think that it can't be proven w/o additional axioms.
Do you know how to prove the lemma?

thank you,
Anton Podkopaev
podkopaev.net

[Anton Podkopaev]

Hello again,

I have found a lemma functional_choice (
https://coq.inria.fr/library/Coq.Logic.IndefiniteDescription.html),
which is exactly what I need.
Sorry for bothering.

thanks,
Anton Podkopaev
podkopaev.net

Post by Anton Podkopaev
Hello,
I'm trying to define a function pointwise. To do so, I'd like to prove the
Definition pointwise_func_def {A B} (P : B -> Prop)
exists (f : A -> B), forall n, P (f n).
I think that it can't be proven w/o additional axioms.
Do you know how to prove the lemma?
thank you,
Anton Podkopaev
podkopaev.net