aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
ModeNameSize
-rw-r--r--Alembert.v28629logplain
-rw-r--r--AltSeries.v16171logplain
-rw-r--r--ArithProp.v7221logplain
-rw-r--r--Binomial.v7938logplain
-rw-r--r--Cauchy_prod.v15679logplain
-rw-r--r--Cos_plus.v26836logplain
-rw-r--r--Cos_rel.v11882logplain
-rw-r--r--DiscrR.v2575logplain
-rw-r--r--Exp_prop.v31616logplain
-rw-r--r--Integration.v623logplain
-rw-r--r--LegacyRfield.v1239logplain
-rw-r--r--MVT.v25892logplain
-rw-r--r--NewtonInt.v29522logplain
-rw-r--r--PSeries_reg.v9559logplain
-rw-r--r--PartSum.v20710logplain
-rw-r--r--RIneq.v56818logplain
-rw-r--r--RList.v27910logplain
-rw-r--r--R_Ifp.v39851logplain
-rw-r--r--R_sqr.v12166logplain
-rw-r--r--R_sqrt.v15278logplain
-rw-r--r--Ranalysis.v29721logplain
-rw-r--r--Ranalysis1.v53545logplain
-rw-r--r--Ranalysis2.v17045logplain
-rw-r--r--Ranalysis3.v30493logplain
-rw-r--r--Ranalysis4.v13151logplain
-rw-r--r--Raxioms.v5139logplain
-rw-r--r--Rbase.v638logplain
-rw-r--r--Rbasic_fun.v18146logplain
-rw-r--r--Rcomplete.v6929logplain
-rw-r--r--Rdefinitions.v2108logplain
-rw-r--r--Rderiv.v22421logplain
-rw-r--r--Reals.v1415logplain
-rw-r--r--Rfunctions.v25582logplain
-rw-r--r--Rgeom.v7873logplain
-rw-r--r--RiemannInt.v140886logplain
-rw-r--r--RiemannInt_SF.v114470logplain
-rw-r--r--Rlimit.v21471logplain
-rw-r--r--Rlogic.v8329logplain
-rw-r--r--Rpow_def.v142logplain
-rw-r--r--Rpower.v24537logplain
-rw-r--r--Rprod.v6629logplain
-rw-r--r--Rseries.v10219logplain
-rw-r--r--Rsigma.v5068logplain
-rw-r--r--Rsqrt_def.v22532logplain
-rw-r--r--Rtopology.v78063logplain
-rw-r--r--Rtrigo.v66404logplain
-rw-r--r--Rtrigo_alt.v17852logplain
-rw-r--r--Rtrigo_calc.v16144logplain
-rw-r--r--Rtrigo_def.v15170logplain
-rw-r--r--Rtrigo_fun.v5313logplain
-rw-r--r--Rtrigo_reg.v23140logplain
-rw-r--r--SeqProp.v43800logplain
-rw-r--r--SeqSeries.v16178logplain
-rw-r--r--SplitAbsolu.v925logplain
-rw-r--r--SplitRmult.v790logplain
-rw-r--r--Sqrt_reg.v13460logplain
-rw-r--r--intro.tex122logplain