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
28872
log
plain
-rw-r--r--
AltSeries.v
16283
log
plain
-rw-r--r--
ArithProp.v
7222
log
plain
-rw-r--r--
Binomial.v
7938
log
plain
-rw-r--r--
Cauchy_prod.v
15679
log
plain
-rw-r--r--
Cos_plus.v
26844
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
31706
log
plain
-rw-r--r--
Integration.v
623
log
plain
-rw-r--r--
MVT.v
25925
log
plain
-rw-r--r--
NewtonInt.v
29717
log
plain
-rw-r--r--
PSeries_reg.v
9680
log
plain
-rw-r--r--
PartSum.v
20726
log
plain
-rw-r--r--
RIneq.v
50112
log
plain
-rw-r--r--
RList.v
27910
log
plain
-rw-r--r--
R_Ifp.v
39851
log
plain
-rw-r--r--
R_sqr.v
12166
log
plain
-rw-r--r--
R_sqrt.v
15278
log
plain
-rw-r--r--
Ranalysis.v
29796
log
plain
-rw-r--r--
Ranalysis1.v
53597
log
plain
-rw-r--r--
Ranalysis2.v
17045
log
plain
-rw-r--r--
Ranalysis3.v
30509
log
plain
-rw-r--r--
Ranalysis4.v
13239
log
plain
-rw-r--r--
Raxioms.v
5147
log
plain
-rw-r--r--
Rbase.v
638
log
plain
-rw-r--r--
Rbasic_fun.v
18146
log
plain
-rw-r--r--
Rcomplete.v
6947
log
plain
-rw-r--r--
Rdefinitions.v
2104
log
plain
-rw-r--r--
Rderiv.v
22421
log
plain
-rw-r--r--
Reals.v
1415
log
plain
-rw-r--r--
Rfunctions.v
25717
log
plain
-rw-r--r--
Rgeom.v
7873
log
plain
-rw-r--r--
RiemannInt.v
141039
log
plain
-rw-r--r--
RiemannInt_SF.v
114895
log
plain
-rw-r--r--
Rlimit.v
21453
log
plain
-rw-r--r--
Rpower.v
24032
log
plain
-rw-r--r--
Rprod.v
5851
log
plain
-rw-r--r--
Rseries.v
10217
log
plain
-rw-r--r--
Rsigma.v
5076
log
plain
-rw-r--r--
Rsqrt_def.v
22691
log
plain
-rw-r--r--
Rtopology.v
78064
log
plain
-rw-r--r--
Rtrigo.v
66347
log
plain
-rw-r--r--
Rtrigo_alt.v
17858
log
plain
-rw-r--r--
Rtrigo_calc.v
16144
log
plain
-rw-r--r--
Rtrigo_def.v
15256
log
plain
-rw-r--r--
Rtrigo_fun.v
5381
log
plain
-rw-r--r--
Rtrigo_reg.v
23260
log
plain
-rw-r--r--
SeqProp.v
43810
log
plain
-rw-r--r--
SeqSeries.v
16300
log
plain
-rw-r--r--
SplitAbsolu.v
925
log
plain
-rw-r--r--
SplitRmult.v
790
log
plain
-rw-r--r--
Sqrt_reg.v
13470
log
plain
-rw-r--r--
intro.tex
122
log
plain