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
27350
log
plain
-rw-r--r--
AltSeries.v
15524
log
plain
-rw-r--r--
ArithProp.v
6828
log
plain
-rw-r--r--
Binomial.v
7527
log
plain
-rw-r--r--
Cauchy_prod.v
14907
log
plain
-rw-r--r--
Cos_plus.v
25475
log
plain
-rw-r--r--
Cos_rel.v
12026
log
plain
-rw-r--r--
DiscrR.v
2575
log
plain
-rw-r--r--
Exp_prop.v
29856
log
plain
-rw-r--r--
Integration.v
623
log
plain
-rw-r--r--
MVT.v
24516
log
plain
-rw-r--r--
NewtonInt.v
28085
log
plain
-rw-r--r--
PSeries_reg.v
9255
log
plain
-rw-r--r--
PartSum.v
19561
log
plain
-rw-r--r--
RIneq.v
47417
log
plain
-rw-r--r--
RList.v
26066
log
plain
-rw-r--r--
R_Ifp.v
25314
log
plain
-rw-r--r--
R_sqr.v
11248
log
plain
-rw-r--r--
R_sqrt.v
14323
log
plain
-rw-r--r--
Ranalysis.v
28528
log
plain
-rw-r--r--
Ranalysis1.v
50356
log
plain
-rw-r--r--
Ranalysis2.v
16250
log
plain
-rw-r--r--
Ranalysis3.v
28778
log
plain
-rw-r--r--
Ranalysis4.v
12455
log
plain
-rw-r--r--
Raxioms.v
5147
log
plain
-rw-r--r--
Rbase.v
638
log
plain
-rw-r--r--
Rbasic_fun.v
17112
log
plain
-rw-r--r--
Rcomplete.v
6589
log
plain
-rw-r--r--
Rdefinitions.v
2163
log
plain
-rw-r--r--
Rderiv.v
18426
log
plain
-rw-r--r--
Reals.v
1414
log
plain
-rw-r--r--
Rfunctions.v
24723
log
plain
-rw-r--r--
Rgeom.v
7520
log
plain
-rw-r--r--
RiemannInt.v
132218
log
plain
-rw-r--r--
RiemannInt_SF.v
107613
log
plain
-rw-r--r--
Rlimit.v
19878
log
plain
-rw-r--r--
Rpower.v
22676
log
plain
-rw-r--r--
Rprod.v
5574
log
plain
-rw-r--r--
Rseries.v
9313
log
plain
-rw-r--r--
Rsigma.v
4657
log
plain
-rw-r--r--
Rsqrt_def.v
21217
log
plain
-rw-r--r--
Rtopology.v
73238
log
plain
-rw-r--r--
Rtrigo.v
61177
log
plain
-rw-r--r--
Rtrigo_alt.v
16897
log
plain
-rw-r--r--
Rtrigo_calc.v
15199
log
plain
-rw-r--r--
Rtrigo_def.v
14524
log
plain
-rw-r--r--
Rtrigo_fun.v
5108
log
plain
-rw-r--r--
Rtrigo_reg.v
22004
log
plain
-rw-r--r--
SeqProp.v
41224
log
plain
-rw-r--r--
SeqSeries.v
15451
log
plain
-rw-r--r--
SplitAbsolu.v
918
log
plain
-rw-r--r--
SplitRmult.v
788
log
plain
-rw-r--r--
Sqrt_reg.v
12744
log
plain
-rw-r--r--
intro.tex
122
log
plain