index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Reals
Mode
Name
Size
-rw-r--r--
Alembert.v
25936
log
plain
-rw-r--r--
AltSeries.v
15615
log
plain
-rw-r--r--
ArithProp.v
6272
log
plain
-rw-r--r--
Binomial.v
7269
log
plain
-rw-r--r--
Cauchy_prod.v
14060
log
plain
-rw-r--r--
Cos_plus.v
32893
log
plain
-rw-r--r--
Cos_rel.v
13981
log
plain
-rw-r--r--
DiscrR.v
2723
log
plain
-rw-r--r--
Exp_prop.v
30180
log
plain
-rw-r--r--
Integration.v
616
log
plain
-rw-r--r--
MVT.v
23188
log
plain
-rw-r--r--
NewtonInt.v
27033
log
plain
-rw-r--r--
PSeries_reg.v
8587
log
plain
-rw-r--r--
PartSum.v
18310
log
plain
-rw-r--r--
RIneq.v
45002
log
plain
-rw-r--r--
RList.v
22603
log
plain
-rw-r--r--
R_Ifp.v
26976
log
plain
-rw-r--r--
R_sqr.v
10856
log
plain
-rw-r--r--
R_sqrt.v
13148
log
plain
-rw-r--r--
Ranalysis.v
23703
log
plain
-rw-r--r--
Ranalysis1.v
46541
log
plain
-rw-r--r--
Ranalysis2.v
16029
log
plain
-rw-r--r--
Ranalysis3.v
27765
log
plain
-rw-r--r--
Ranalysis4.v
11729
log
plain
-rw-r--r--
Raxioms.v
5750
log
plain
-rw-r--r--
Rbase.v
658
log
plain
-rw-r--r--
Rbasic_fun.v
17491
log
plain
-rw-r--r--
Rcomplete.v
6413
log
plain
-rw-r--r--
Rdefinitions.v
1466
log
plain
-rw-r--r--
Rderiv.v
20776
log
plain
-rw-r--r--
Reals.v
1408
log
plain
-rw-r--r--
Rfunctions.v
24724
log
plain
-rw-r--r--
Rgeom.v
6552
log
plain
-rw-r--r--
RiemannInt.v
124974
log
plain
-rw-r--r--
RiemannInt_SF.v
99713
log
plain
-rw-r--r--
Rlimit.v
21226
log
plain
-rw-r--r--
Rpower.v
22330
log
plain
-rw-r--r--
Rprod.v
6704
log
plain
-rw-r--r--
Rseries.v
9704
log
plain
-rw-r--r--
Rsigma.v
5136
log
plain
-rw-r--r--
Rsqrt_def.v
19690
log
plain
-rw-r--r--
Rsyntax.v
9127
log
plain
-rw-r--r--
Rtopology.v
67402
log
plain
-rw-r--r--
Rtrigo.v
57465
log
plain
-rw-r--r--
Rtrigo_alt.v
18228
log
plain
-rw-r--r--
Rtrigo_calc.v
13782
log
plain
-rw-r--r--
Rtrigo_def.v
14786
log
plain
-rw-r--r--
Rtrigo_fun.v
5389
log
plain
-rw-r--r--
Rtrigo_reg.v
21434
log
plain
-rw-r--r--
SeqProp.v
40008
log
plain
-rw-r--r--
SeqSeries.v
14450
log
plain
-rw-r--r--
SplitAbsolu.v
920
log
plain
-rw-r--r--
SplitRmult.v
769
log
plain
-rw-r--r--
Sqrt_reg.v
12012
log
plain
-rw-r--r--
TypeSyntax.v
774
log
plain
-rw-r--r--
intro.tex
122
log
plain