aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
ModeNameSize
-rw-r--r--.cvsignore5logplain
-rw-r--r--Alembert.v27335logplain
-rw-r--r--AltSeries.v15791logplain
-rw-r--r--ArithProp.v6800logplain
-rw-r--r--Binomial.v7527logplain
-rw-r--r--Cauchy_prod.v14778logplain
-rw-r--r--Cos_plus.v31828logplain
-rw-r--r--Cos_rel.v12957logplain
-rw-r--r--DiscrR.v2989logplain
-rw-r--r--Exp_prop.v31366logplain
-rw-r--r--Integration.v623logplain
-rw-r--r--MVT.v24496logplain
-rw-r--r--NewtonInt.v28069logplain
-rw-r--r--PSeries_reg.v9255logplain
-rw-r--r--PartSum.v19631logplain
-rw-r--r--RIneq.v47445logplain
-rw-r--r--RList.v26066logplain
-rw-r--r--R_Ifp.v25313logplain
-rw-r--r--R_sqr.v11248logplain
-rw-r--r--R_sqrt.v14323logplain
-rw-r--r--Ranalysis.v28512logplain
-rw-r--r--Ranalysis1.v49742logplain
-rw-r--r--Ranalysis2.v16250logplain
-rw-r--r--Ranalysis3.v28723logplain
-rw-r--r--Ranalysis4.v12432logplain
-rw-r--r--Raxioms.v5147logplain
-rw-r--r--Rbase.v637logplain
-rw-r--r--Rbasic_fun.v17062logplain
-rw-r--r--Rcomplete.v6589logplain
-rw-r--r--Rdefinitions.v2163logplain
-rw-r--r--Rderiv.v18426logplain
-rw-r--r--Reals.v1414logplain
-rw-r--r--Rfunctions.v24781logplain
-rw-r--r--Rgeom.v7510logplain
-rw-r--r--RiemannInt.v132218logplain
-rw-r--r--RiemannInt_SF.v108254logplain
-rw-r--r--Rlimit.v19878logplain
-rw-r--r--Rpower.v22697logplain
-rw-r--r--Rprod.v7153logplain
-rw-r--r--Rseries.v9313logplain
-rw-r--r--Rsigma.v5319logplain
-rw-r--r--Rsqrt_def.v21212logplain
-rw-r--r--Rtopology.v73238logplain
-rw-r--r--Rtrigo.v61307logplain
-rw-r--r--Rtrigo_alt.v17888logplain
-rw-r--r--Rtrigo_calc.v15199logplain
-rw-r--r--Rtrigo_def.v14524logplain
-rw-r--r--Rtrigo_fun.v5151logplain
-rw-r--r--Rtrigo_reg.v22151logplain
-rw-r--r--SeqProp.v41690logplain
-rw-r--r--SeqSeries.v15436logplain
-rw-r--r--SplitAbsolu.v918logplain
-rw-r--r--SplitRmult.v788logplain
-rw-r--r--Sqrt_reg.v12744logplain
-rw-r--r--intro.tex122logplain