aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Collapse)Author
2002-09-25preuve d'un axiome restant via Rtopologydesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3036 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25MAJ pour Rtopologydesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3035 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25Proprietes topologiques dans Rdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3034 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31MAJ pour TAFdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2950 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31Theoreme des accroissements finis generalises et corollairesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2948 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31MAJ pour Exp_propdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2946 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31Proprietes de l'exponentielledesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2945 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29MAJ pour Rtrigo_regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2934 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29Regularite de sin et cosdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2933 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29Continuite des series de fonctions NCdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2932 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-22Quelques ameliorations dans Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2907 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19Nvll preuves R_dist_tri et tech_limitmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2906 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19Regularites de pow et des sommes finies / MAJ Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2904 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19Resultats de regularite de Rabsolu / MAJ de Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2903 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19Quelques ameliorations...desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2902 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18Correction d'un bug dans IsCont_ptdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2899 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18MAJ pour Sqrt_regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2898 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18Preuves de la continuite/derivabilite de sqrt sur R+/R+*desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2897 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2884 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2883 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Rtrigo pour sqrtdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2880 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2879 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16R_sqr ne contient plus de resultats sur sqrt -> R_sqrtdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2878 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Realsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2877 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16MAJ Rgeomdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2876 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Proprietes (calculatoires) des fonctions trigonometriquesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2875 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Proprietes de la racine carreedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2874 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Definition de la racine carreedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2873 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Preuve de cos_plusdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2863 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Quelques resultats supplementaires sur les suites convergentesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2862 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Le theoreme central sur les produits de Cauchy finisdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2861 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12Differents resultats sur les produits finisdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2860 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-12cos_plus prouvedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2858 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05certains lemmes sont maintenant dans Rtrigodesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2844 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05sin_plus prouve (a partir de cos_plus)desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2843 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05sin_bound et cos_bound deplaces dans Rtrigo_altdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2842 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05sin_bound et cos_bound sont prouves (merci les series alternees...)desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2841 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-03*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2836 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-03sin_eq_0 est maintenant prouvedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2835 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02sin_lb_gt_0 est maintenant prouve (grace a une approximation de PI, cf PI_ineq)desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2830 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02Suppression de l'axiome arc_sin_cosdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2823 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02Modification de IAF, introduction de TAF et preuves de 3 axiomesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2822 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2821 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Constructions des séries alternées et de PIdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2819 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01PI n'est plus un axiomedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2818 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Version plus propre de Rsigmadesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2815 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Ajout de Binomedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2814 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Formule du binome (pour cos(x+y), sin(x+y)...)desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2813 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-01Modification sin_approxdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2812 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-26Resolution de bug (du a Auto; remplacement par lt_O_Sn)mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2807 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 21:56:13 +0000