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
25910
log
plain
-rw-r--r--
AltSeries.v
15589
log
plain
-rw-r--r--
ArithProp.v
6220
log
plain
-rw-r--r--
Binomial.v
7243
log
plain
-rw-r--r--
Cauchy_prod.v
14034
log
plain
-rw-r--r--
Cos_plus.v
32839
log
plain
-rw-r--r--
Cos_rel.v
13955
log
plain
-rw-r--r--
DiscrR.v
2697
log
plain
-rw-r--r--
Exp_prop.v
30093
log
plain
-rw-r--r--
Integration.v
616
log
plain
-rw-r--r--
MVT.v
23162
log
plain
-rw-r--r--
NewtonInt.v
27007
log
plain
-rw-r--r--
PSeries_reg.v
8561
log
plain
-rw-r--r--
PartSum.v
18284
log
plain
-rw-r--r--
RIneq.v
44753
log
plain
-rw-r--r--
RList.v
22577
log
plain
-rw-r--r--
R_Ifp.v
26949
log
plain
-rw-r--r--
R_sqr.v
10830
log
plain
-rw-r--r--
R_sqrt.v
13122
log
plain
-rw-r--r--
Ranalysis.v
23677
log
plain
-rw-r--r--
Ranalysis1.v
46509
log
plain
-rw-r--r--
Ranalysis2.v
16003
log
plain
-rw-r--r--
Ranalysis3.v
27739
log
plain
-rw-r--r--
Ranalysis4.v
11703
log
plain
-rw-r--r--
Raxioms.v
5229
log
plain
-rw-r--r--
Rbase.v
658
log
plain
-rw-r--r--
Rbasic_fun.v
17463
log
plain
-rw-r--r--
Rcomplete.v
6387
log
plain
-rw-r--r--
Rdefinitions.v
1466
log
plain
-rw-r--r--
Rderiv.v
20750
log
plain
-rw-r--r--
Reals.v
1408
log
plain
-rw-r--r--
Rfunctions.v
24981
log
plain
-rw-r--r--
Rgeom.v
6526
log
plain
-rw-r--r--
RiemannInt.v
124948
log
plain
-rw-r--r--
RiemannInt_SF.v
99687
log
plain
-rw-r--r--
Rlimit.v
21200
log
plain
-rw-r--r--
Rpower.v
22304
log
plain
-rw-r--r--
Rprod.v
6678
log
plain
-rw-r--r--
Rseries.v
9704
log
plain
-rw-r--r--
Rsigma.v
5110
log
plain
-rw-r--r--
Rsqrt_def.v
19664
log
plain
-rw-r--r--
Rsyntax.v
8956
log
plain
-rw-r--r--
Rtopology.v
67376
log
plain
-rw-r--r--
Rtrigo.v
57383
log
plain
-rw-r--r--
Rtrigo_alt.v
18202
log
plain
-rw-r--r--
Rtrigo_calc.v
13756
log
plain
-rw-r--r--
Rtrigo_def.v
14760
log
plain
-rw-r--r--
Rtrigo_fun.v
5389
log
plain
-rw-r--r--
Rtrigo_reg.v
21342
log
plain
-rw-r--r--
SeqProp.v
40354
log
plain
-rw-r--r--
SeqSeries.v
14424
log
plain
-rw-r--r--
SplitAbsolu.v
920
log
plain
-rw-r--r--
SplitRmult.v
769
log
plain
-rw-r--r--
Sqrt_reg.v
11986
log
plain
-rw-r--r--
TypeSyntax.v
1223
log
plain
-rw-r--r--
intro.tex
122
log
plain