summaryrefslogtreecommitdiff
path: root/theories/Reals
ModeNameSize
-rw-r--r--Alembert.v28917logplain
-rw-r--r--AltSeries.v16320logplain
-rw-r--r--ArithProp.v7270logplain
-rw-r--r--Binomial.v7983logplain
-rw-r--r--Cauchy_prod.v15727logplain
-rw-r--r--Cos_plus.v26884logplain
-rw-r--r--Cos_rel.v11926logplain
-rw-r--r--DiscrR.v2619logplain
-rw-r--r--Exp_prop.v31714logplain
-rw-r--r--Integration.v674logplain
-rw-r--r--LegacyRfield.v1239logplain
-rw-r--r--MVT.v25965logplain
-rw-r--r--NewtonInt.v29763logplain
-rw-r--r--PSeries_reg.v9728logplain
-rw-r--r--PartSum.v20769logplain
-rw-r--r--RIneq.v49599logplain
-rw-r--r--RList.v27952logplain
-rw-r--r--R_Ifp.v39893logplain
-rw-r--r--R_sqr.v12208logplain
-rw-r--r--R_sqrt.v15321logplain
-rw-r--r--Ranalysis.v29768logplain
-rw-r--r--Ranalysis1.v53644logplain
-rw-r--r--Ranalysis2.v17092logplain
-rw-r--r--Ranalysis3.v30556logplain
-rw-r--r--Ranalysis4.v13286logplain
-rw-r--r--Raxioms.v5191logplain
-rw-r--r--Rbase.v681logplain
-rw-r--r--Rbasic_fun.v18193logplain
-rw-r--r--Rcomplete.v6993logplain
-rw-r--r--Rdefinitions.v2170logplain
-rw-r--r--Rderiv.v22464logplain
-rw-r--r--Reals.v1457logplain
-rw-r--r--Rfunctions.v25556logplain
-rw-r--r--Rgeom.v7915logplain
-rw-r--r--RiemannInt.v141086logplain
-rw-r--r--RiemannInt_SF.v114945logplain
-rw-r--r--Rlimit.v21496logplain
-rw-r--r--Rpow_def.v142logplain
-rw-r--r--Rpower.v24075logplain
-rw-r--r--Rprod.v5893logplain
-rw-r--r--Rseries.v10261logplain
-rw-r--r--Rsigma.v5114logplain
-rw-r--r--Rsqrt_def.v22719logplain
-rw-r--r--Rtopology.v78110logplain
-rw-r--r--Rtrigo.v66450logplain
-rw-r--r--Rtrigo_alt.v17900logplain
-rw-r--r--Rtrigo_calc.v16192logplain
-rw-r--r--Rtrigo_def.v15303logplain
-rw-r--r--Rtrigo_fun.v5428logplain
-rw-r--r--Rtrigo_reg.v23302logplain
-rw-r--r--SeqProp.v43841logplain
-rw-r--r--SeqSeries.v16346logplain
-rw-r--r--SplitAbsolu.v973logplain
-rw-r--r--SplitRmult.v837logplain
-rw-r--r--Sqrt_reg.v13515logplain
-rw-r--r--intro.tex122logplain