1
<html xmlns="http://www.w3.org/1999/xhtml">
3
<meta http-equiv="Content-Type" content="text/html; charset="><link rel="stylesheet" href="style.css" type="text/css"><title>Coq.Logic.ClassicalChoice</title>
8
<h1>Library Coq.Logic.ClassicalChoice</h1>
13
<table width="100%"><tr class="doc"><td>
14
This file provides classical logic and functional choice
21
<table width="100%"><tr class="doc"><td>
22
This file extends ClassicalDescription.v with the axiom of choice.
23
As ClassicalDescription.v, it implies the double-negation of
24
excluded-middle in Set and implies a strongly classical
25
world. Especially it conflicts with impredicativity of Set, knowing
26
that true<>false in Set.
32
<code class="keyword">Require</code> <code class="keyword">Export</code> <a href="Coq.Logic.ClassicalDescription.html">ClassicalDescription</a>.<br/>
33
<code class="keyword">Require</code> <code class="keyword">Export</code> <a href="Coq.Logic.RelationalChoice.html">RelationalChoice</a>.<br/>
34
<code class="keyword">Require</code> <code class="keyword">Import</code> ChoiceFacts.<br/>
37
<code class="keyword">Theorem</code> <a name="choice"></a>choice :<br/>
38
forall (A B:Type) (R:A -> B -> Prop),<br/>
39
(forall x:A, exists y : B, R x y) -><br/>
40
exists f : A -> B, (forall x:A, R x (f x)).<br/>
41
<code class="keyword">Proof</code>.<br/>
42
apply <a href="Coq.Logic.ChoiceFacts.html#description_rel_choice_imp_funct_choice">description_rel_choice_imp_funct_choice</a>.<br/>
43
exact <a href="Coq.Logic.ClassicalDescription.html#description">description</a>.<br/>
44
exact <a href="Coq.Logic.RelationalChoice.html#relational_choice">relational_choice</a>.<br/>
45
<code class="keyword">Qed</code>.</code>
46
<hr/><a href="index.html">Index</a><hr/><font size="-1">This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a></font>
b'\\ No newline at end of file'
added
removed
library/Coq.Logic.ClassicalChoice.html
