diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-09 13:00:51 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-09 13:00:51 +0000 |
| commit | d63861313993ed3d0a0108d659e0b08a215442c1 (patch) | |
| tree | 14bcf9eda0168fe0f088fb555cde18297037f8ee | |
| parent | 854948d1ebf547ee60414b73e0be1a7827c6d1c8 (diff) | |
Preuve du lemme de Rolle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3109 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/TAF.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/Reals/TAF.v b/theories/Reals/TAF.v index c50714100..d1327f496 100644 --- a/theories/Reals/TAF.v +++ b/theories/Reals/TAF.v @@ -147,6 +147,14 @@ Qed. (*** Corollaires ***) +Lemma Rolle : (f:R->R;a,b:R;pr:(x:R)``a<x<b``->(derivable_pt f x)) ((x:R)``a<=x<=b``->(continuity_pt f x)) -> ``a<b`` -> (f a)==(f b) -> (EXT c:R | (EXT P: ``a<c<b`` | ``(derive_pt f c (pr c P))==0``)). +Intros; Assert H2 : (x:R)``a<x<b``->(derivable_pt id x). +Intros; Apply derivable_pt_id. +Assert H3 := (TAF_gen f id a b pr H2 H0 H); Assert H4 : (x:R)``a<=x<=b``->(continuity_pt id x). +Intros; Apply derivable_continuous; Apply derivable_id. +Elim (H3 H4); Intros; Elim H5; Intros; Exists x; Exists x0; Rewrite H1 in H6; Unfold id in H6; Unfold Rminus in H6; Rewrite Rplus_Ropp_r in H6; Rewrite Rmult_Ol in H6; Apply r_Rmult_mult with ``b-a``; [Rewrite Rmult_Or; Apply H6 | Apply Rminus_eq_contra; Red; Intro; Rewrite H7 in H0; Elim (Rlt_antirefl ? H0)]. +Qed. + (**********) Lemma nonneg_derivative_1 : (f:R->R;pr:(derivable f)) ((x:R) ``0<=(derive_pt f x (pr x))``) -> (increasing f). Intros. |