aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
ModeNameSize
-rw-r--r--Alembert.v27475logplain
-rw-r--r--AltSeries.v15634logplain
-rw-r--r--ArithProp.v6978logplain
-rw-r--r--Binomial.v7611logplain
-rw-r--r--Cauchy_prod.v15543logplain
-rw-r--r--Cos_plus.v25973logplain
-rw-r--r--Cos_rel.v11373logplain
-rw-r--r--DiscrR.v2382logplain
-rw-r--r--Exp_prop.v30251logplain
-rw-r--r--Integration.v609logplain
-rw-r--r--MVT.v25466logplain
-rw-r--r--Machin.v6574logplain
-rw-r--r--NewtonInt.v28862logplain
-rw-r--r--PSeries_reg.v9234logplain
-rw-r--r--PartSum.v20056logplain
-rw-r--r--RIneq.v57475logplain
-rw-r--r--RList.v26777logplain
-rw-r--r--ROrderedType.v2737logplain
-rw-r--r--R_Ifp.v39465logplain
-rw-r--r--R_sqr.v11987logplain
-rw-r--r--R_sqrt.v15987logplain
-rw-r--r--Ranalysis.v1056logplain
-rw-r--r--Ranalysis1.v51355logplain
-rw-r--r--Ranalysis2.v16507logplain
-rw-r--r--Ranalysis3.v29825logplain
-rw-r--r--Ranalysis4.v12653logplain
-rw-r--r--Ranalysis5.v57947logplain
-rw-r--r--Ranalysis_reg.v29646logplain
-rw-r--r--Ratan.v62108logplain
-rw-r--r--Raxioms.v5085logplain
-rw-r--r--Rbase.v624logplain
-rw-r--r--Rbasic_fun.v20898logplain
-rw-r--r--Rcomplete.v6731logplain
-rw-r--r--Rdefinitions.v2126logplain
-rw-r--r--Rderiv.v21670logplain
-rw-r--r--Reals.v1400logplain
-rw-r--r--Rfunctions.v24007logplain
-rw-r--r--Rgeom.v7745logplain
-rw-r--r--RiemannInt.v136796logplain
-rw-r--r--RiemannInt_SF.v109988logplain
-rw-r--r--Rlimit.v20843logplain
-rw-r--r--Rlogic.v5541logplain
-rw-r--r--Rminmax.v3645logplain
-rw-r--r--Rpow_def.v657logplain
-rw-r--r--Rpower.v23842logplain
-rw-r--r--Rprod.v6536logplain
-rw-r--r--Rseries.v12481logplain
-rw-r--r--Rsigma.v4940logplain
-rw-r--r--Rsqrt_def.v21578logplain
-rw-r--r--Rtopology.v74279logplain
-rw-r--r--Rtrigo.v962logplain
-rw-r--r--Rtrigo1.v71156logplain
-rw-r--r--Rtrigo_alt.v16862logplain
-rw-r--r--Rtrigo_calc.v15546logplain
-rw-r--r--Rtrigo_def.v14662logplain
-rw-r--r--Rtrigo_fun.v5217logplain
-rw-r--r--Rtrigo_reg.v16895logplain
-rw-r--r--SeqProp.v37744logplain
-rw-r--r--SeqSeries.v15736logplain
-rw-r--r--SplitAbsolu.v892logplain
-rw-r--r--SplitRmult.v776logplain
-rw-r--r--Sqrt_reg.v12734logplain
-rw-r--r--intro.tex122logplain
-rw-r--r--vo.itarget754logplain