coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Anton Podkopaev <anton AT podkopaev.net>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Pointwise definition of function
- Date: Wed, 15 Aug 2018 16:19:43 +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 forward106j.mail.yandex.net
- Ironport-phdr: 9a23:s8KitxL8rvxCo7AzfNmcpTZWNBhigK39O0sv0rFitYgRLfvxwZ3uMQTl6Ol3ixeRBMOHs6wC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwRFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicJOTA67W/ZlNB/gblBrx69vRFy2ZLYbJ2XOfd4Y6jTfckaRW1EXstJSyFBBJ+8b4wJD+EcJ+hYqJTyp1gJrRumHwajGv3vwSJPi3Ds2606z+MhEQfd0Qw4GNIBrXfUrNLtNKgIT++10rPEzTPdYPNKwDrw7pXDfB4mofGJR71wcMzRxFE3FwPCk1qQqovlPyuP2esTrWiX9exgWvyzi2Mhtgp/oSCvy98sh4XTiY8YykrI+Th9zYs2P9G0VkF2bNq8HJdOrS6WK5V6T8YjTm5zuys3z6EKtJu4cSQW1ZgqwhvSZOacfIWO/xntTvyeIS1ii3JgYL+/hwi98UynyuDkWMm010xKryRfndnWq38BygDf58mFSvdn+0euwzeP1wTJ5uBEO080k7fUJIAuw7IqkJocr1jDEjf3mEXwkqCWal0p9+iy5+noYrjqvIKQOot3hw3kLKgjlciyDfw9MgcUXmib/eq81Kfk/U38WLhFlPs2krXesJDcPskbvqm5DBJW0oYk8xawFSmp0MoCkXkBMl1FZAqLj5L1NFHWPPD4EfC/jkywnzds3vDKJ6HuApHQLnfYi7rhZrZ860tEyAUp19xf5pRUCqsAIP3pQEPxusbYXVcFNFm/xP+iA9Fg3KsfX3iOC+mXKvD8q1iNs8spP+6KLLcStDX6M/Eo+ba6hHklnlk1Za6l3pwPYX2mWPJrPxPKMjLXnt4dHDJS7UIFR+vwhQjaCG8BVzOJR6s5owoDJsejBIbHSJqqheXcjj+8Ep5RfmlLFBaKHGu6LtzYCcdJUzqbJ4paqhJBTaKoEtJzzRaitwjiwrd5aOzZ5n9A7M+x5J1O/+TW0CoK23l0AsCaiTDfQWZugWoSS2ZugqI5pEV8zhGS2K50juweE9FPtatE
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
- [Coq-Club] Pointwise definition of function, Anton Podkopaev, 08/15/2018
- Re: [Coq-Club] Pointwise definition of function, Anton Podkopaev, 08/15/2018
Archive powered by MHonArc 2.6.18.