aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
ModeNameSize
-rw-r--r--Alembert.v28633logplain
-rw-r--r--AltSeries.v16164logplain
-rw-r--r--ArithProp.v7216logplain
-rw-r--r--Binomial.v7937logplain
-rw-r--r--Cauchy_prod.v15677logplain
-rw-r--r--Cos_plus.v26789logplain
-rw-r--r--Cos_rel.v11757logplain
-rw-r--r--DiscrR.v2433logplain
-rw-r--r--Exp_prop.v31613logplain
-rw-r--r--Integration.v622logplain
-rw-r--r--LegacyRfield.v1239logplain
-rw-r--r--MVT.v25880logplain
-rw-r--r--NewtonInt.v29515logplain
-rw-r--r--PSeries_reg.v9552logplain
-rw-r--r--PartSum.v20702logplain
-rw-r--r--RIneq.v57765logplain
-rw-r--r--RList.v27807logplain
-rw-r--r--ROrderedType.v2729logplain
-rw-r--r--R_Ifp.v39788logplain
-rw-r--r--R_sqr.v12152logplain
-rw-r--r--R_sqrt.v16209logplain
-rw-r--r--Ranalysis.v29659logplain
-rw-r--r--Ranalysis1.v53518logplain
-rw-r--r--Ranalysis2.v16913logplain
-rw-r--r--Ranalysis3.v30487logplain
-rw-r--r--Ranalysis4.v13138logplain
-rw-r--r--Raxioms.v5125logplain
-rw-r--r--Rbase.v638logplain
-rw-r--r--Rbasic_fun.v21294logplain
-rw-r--r--Rcomplete.v6929logplain
-rw-r--r--Rdefinitions.v2140logplain
-rw-r--r--Rderiv.v22259logplain
-rw-r--r--Reals.v1413logplain
-rw-r--r--Rfunctions.v25778logplain
-rw-r--r--Rgeom.v7870logplain
-rw-r--r--RiemannInt.v140800logplain
-rw-r--r--RiemannInt_SF.v114322logplain
-rw-r--r--Rlimit.v21398logplain
-rw-r--r--Rlogic.v8322logplain
-rw-r--r--Rminmax.v3645logplain
-rw-r--r--Rpow_def.v669logplain
-rw-r--r--Rpower.v24526logplain
-rw-r--r--Rprod.v6606logplain
-rw-r--r--Rseries.v12647logplain
-rw-r--r--Rsigma.v5068logplain
-rw-r--r--Rsqrt_def.v22526logplain
-rw-r--r--Rtopology.v77957logplain
-rw-r--r--Rtrigo.v66378logplain
-rw-r--r--Rtrigo_alt.v17838logplain
-rw-r--r--Rtrigo_calc.v16137logplain
-rw-r--r--Rtrigo_def.v15164logplain
-rw-r--r--Rtrigo_fun.v5305logplain
-rw-r--r--Rtrigo_reg.v23135logplain
-rw-r--r--SeqProp.v38893logplain
-rw-r--r--SeqSeries.v16173logplain
-rw-r--r--SplitAbsolu.v925logplain
-rw-r--r--SplitRmult.v790logplain
-rw-r--r--Sqrt_reg.v13452logplain
-rw-r--r--intro.tex122logplain
-rw-r--r--vo.itarget709logplain