coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pointwise definition of function

From: Anton Podkopaev <anton AT podkopaev.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Pointwise definition of function
Date: Wed, 15 Aug 2018 17:33:55 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=anton AT podkopaev.net; spf=Pass smtp.mailfrom=anton AT podkopaev.net; spf=None smtp.helo=postmaster AT forward106p.mail.yandex.net
Ironport-phdr: 9a23:QJvSwBwJ8dr+z8PXCy+O+j09IxM/srCxBDY+r6Qd1OMfIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRDqhicJNzA3/mLKhMJukK1WuwiuqwBlzoPOfI2ZKPhzc6XAdt0aX2pBWcNRWjRdD4O6c4sPCOwBNvtCoYn6ulQOrhy+BRG2C+zx1D9Dm3j70rc80+Q9FgHG2hctH8oJsHvJr9X1M78SXvqrw6nW1znDae1Z2Svk5YXObxsvr/aMXbdqfsrQz0kiDwLFjlOKqYzkJTyZzOoNs3KD4+p4UuKglm0nqwZpoje12MgslJPFhoQLxVDY8yhy3YU7JcWgRUN5Y9OoCphduiKAO4doQc4uWXxktDo+x7Eep5K0ZjQGxIoiyhPecPOKcI2F7g7mWeuSPTt0mXdodbeliBmp90Wr1/fyWdOu0FlQqypIitnMuW4J1xzU8sWHRPx9/l2v2DmVzQDc9/xILVw1mKrDMZIhx6Q/lpsXsUjZHi75gkP2g7KIeUQr4OSo7froYqn+qp+dMY97lB3+P7wsl8G9G+g1MQsDU3KF9em/zrHv4FH1TbFSgv0ziKbZsZTaJcoBpq6+Bg9Yypws6xCjDzeh1tQVhmEHLFVYdxKEiIjpI0vBL+7mDfulhVSjjitry+jcPrL9GpXNMmTDkLD5cLlh7E5c0RM/wsxb55JJEb4MO+nzW0/0tNzAFBA1KQ20w+D9CNV8zIwSQ2yPArXKeJ/V5FSP/6ckJ/SGTI4Tojf0bfY/tND0inpssFkBeq/h5Zwba3egF/l4axGQZ2brhP8ZFmsJuRI3QfKsjlCeB20AL02uVr4xs2loQLmtCp3OE9j00e6xmRyjF5gTXVhoT1WFEHPmbYKBAqpecCWeIch5mzEaE76sV914jE38hErB07Nia9Hs1GgAr5u6iYpt4OHQkgk7+CIyCcmBgTnUEjNE21gQTjpz55hR5ExwzlDZgPp2hOZHHMZfvqsXSkE/PJ/Yif1zDdz/SkTHc8vbEFs=

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

On Wed, Aug 15, 2018 at 4:19 PM, Anton Podkopaev <anton AT podkopaev.net> wrote:

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

[Coq-Club] Pointwise definition of function, Anton Podkopaev, 08/15/2018
- Re: [Coq-Club] Pointwise definition of function, Anton Podkopaev, 08/15/2018