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.Reals.Rdefinitions</title>
8
<h1>Library Coq.Reals.Rdefinitions</h1>
13
<table width="100%"><tr class="doc"><td>
14
Definitions for the axiomatization
17
<code class="keyword">Require</code> <code class="keyword">Export</code> <a href="Coq.ZArith.ZArith_base.html">ZArith_base</a>.<br/>
20
<code class="keyword">Parameter</code> <a name="R"></a>R : Set.<br/>
23
Delimit Scope R_scope with R.<br/>
26
Bind Scope R_scope with R.<br/>
29
<code class="keyword">Parameter</code> <a name="R0"></a>R0 : <a href="Coq.Reals.Rdefinitions.html#R">R</a>.<br/>
30
<code class="keyword">Parameter</code> <a name="R1"></a>R1 : <a href="Coq.Reals.Rdefinitions.html#R">R</a>.<br/>
31
<code class="keyword">Parameter</code> <a name="Rplus"></a>Rplus : <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>.<br/>
32
<code class="keyword">Parameter</code> <a name="Rmult"></a>Rmult : <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>.<br/>
33
<code class="keyword">Parameter</code> <a name="Ropp"></a>Ropp : <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>.<br/>
34
<code class="keyword">Parameter</code> <a name="Rinv"></a>Rinv : <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>. <br/>
35
<code class="keyword">Parameter</code> <a name="Rlt"></a>Rlt : <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> Prop. <br/>
36
<code class="keyword">Parameter</code> <a name="up"></a>up : <a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.ZArith.BinInt.html#Z">Z</a>.<br/>
39
<code class="keyword">Infix</code> "+" := <a href="Coq.Reals.Rdefinitions.html#Rplus">Rplus</a> : R_scope.<br/>
40
<code class="keyword">Infix</code> "*" := <a href="Coq.Reals.Rdefinitions.html#Rmult">Rmult</a> : R_scope.<br/>
41
<code class="keyword">Notation</code> "- x" := (<a href="Coq.Reals.Rdefinitions.html#Ropp">Ropp</a> x) : R_scope.<br/>
42
<code class="keyword">Notation</code> "/ x" := (<a href="Coq.Reals.Rdefinitions.html#Rinv">Rinv</a> x) : R_scope.<br/>
45
<code class="keyword">Infix</code> "<" := <a href="Coq.Reals.Rdefinitions.html#Rlt">Rlt</a> : R_scope.<br/>
48
<code class="keyword">Definition</code> <a name="Rgt"></a>Rgt (r1 r2:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : Prop := (r2 < r1)%R.<br/>
51
<code class="keyword">Definition</code> <a name="Rle"></a>Rle (r1 r2:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : Prop := (r1 < r2)%R \/ r1 = r2.<br/>
54
<code class="keyword">Definition</code> <a name="Rge"></a>Rge (r1 r2:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : Prop := <a href="Coq.Reals.Rdefinitions.html#Rgt">Rgt</a> r1 r2 \/ r1 = r2.<br/>
57
<code class="keyword">Definition</code> <a name="Rminus"></a>Rminus (r1 r2:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> := (r1 + - r2)%R.<br/>
60
<code class="keyword">Definition</code> <a name="Rdiv"></a>Rdiv (r1 r2:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> := (r1 * / r2)%R.<br/>
63
<code class="keyword">Infix</code> "-" := <a href="Coq.Reals.Rdefinitions.html#Rminus">Rminus</a> : R_scope.<br/>
64
<code class="keyword">Infix</code> "/" := <a href="Coq.Reals.Rdefinitions.html#Rdiv">Rdiv</a> : R_scope.<br/>
67
<code class="keyword">Infix</code> "<=" := <a href="Coq.Reals.Rdefinitions.html#Rle">Rle</a> : R_scope.<br/>
68
<code class="keyword">Infix</code> ">=" := <a href="Coq.Reals.Rdefinitions.html#Rge">Rge</a> : R_scope.<br/>
69
<code class="keyword">Infix</code> ">" := <a href="Coq.Reals.Rdefinitions.html#Rgt">Rgt</a> : R_scope.<br/>
72
<code class="keyword">Notation</code> "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope.<br/>
73
<code class="keyword">Notation</code> "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope.<br/>
74
<code class="keyword">Notation</code> "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope.<br/>
75
<code class="keyword">Notation</code> "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope.</code>
76
<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.Reals.Rdefinitions.html
