summaryrefslogtreecommitdiff
path: root/theories/Reals
ModeNameSize
-rw-r--r--Alembert.v27398logplain
-rw-r--r--AltSeries.v15840logplain
-rw-r--r--ArithProp.v6849logplain
-rw-r--r--Binomial.v7575logplain
-rw-r--r--Cauchy_prod.v14829logplain
-rw-r--r--Cos_plus.v31876logplain
-rw-r--r--Cos_rel.v13002logplain
-rw-r--r--DiscrR.v3035logplain
-rw-r--r--Exp_prop.v31416logplain
-rw-r--r--Integration.v674logplain
-rw-r--r--MVT.v24559logplain
-rw-r--r--NewtonInt.v28134logplain
-rw-r--r--PSeries_reg.v9306logplain
-rw-r--r--PartSum.v19683logplain
-rw-r--r--RIneq.v47490logplain
-rw-r--r--RList.v26111logplain
-rw-r--r--R_Ifp.v25358logplain
-rw-r--r--R_sqr.v11293logplain
-rw-r--r--R_sqrt.v14369logplain
-rw-r--r--Ranalysis.v28561logplain
-rw-r--r--Ranalysis1.v49937logplain
-rw-r--r--Ranalysis2.v16300logplain
-rw-r--r--Ranalysis3.v28828logplain
-rw-r--r--Ranalysis4.v12505logplain
-rw-r--r--Raxioms.v5194logplain
-rw-r--r--Rbase.v682logplain
-rw-r--r--Rbasic_fun.v17112logplain
-rw-r--r--Rcomplete.v6638logplain
-rw-r--r--Rdefinitions.v2215logplain
-rw-r--r--Rderiv.v18472logplain
-rw-r--r--Reals.v1459logplain
-rw-r--r--Rfunctions.v24831logplain
-rw-r--r--Rgeom.v7555logplain
-rw-r--r--RiemannInt.v132268logplain
-rw-r--r--RiemannInt_SF.v108307logplain
-rw-r--r--Rlimit.v19924logplain
-rw-r--r--Rpower.v22743logplain
-rw-r--r--Rprod.v7198logplain
-rw-r--r--Rseries.v9360logplain
-rw-r--r--Rsigma.v5365logplain
-rw-r--r--Rsqrt_def.v21266logplain
-rw-r--r--Rtopology.v73287logplain
-rw-r--r--Rtrigo.v61351logplain
-rw-r--r--Rtrigo_alt.v17936logplain
-rw-r--r--Rtrigo_calc.v15250logplain
-rw-r--r--Rtrigo_def.v14574logplain
-rw-r--r--Rtrigo_fun.v5157logplain
-rw-r--r--Rtrigo_reg.v22206logplain
-rw-r--r--SeqProp.v41563logplain
-rw-r--r--SeqSeries.v15500logplain
-rw-r--r--SplitAbsolu.v969logplain
-rw-r--r--SplitRmult.v838logplain
-rw-r--r--Sqrt_reg.v12792logplain
-rw-r--r--intro.tex122logplain