proposition: Lemma prolongement_C0 : forall (f:R -> R) (a b:R), a <= b -> (forall c:R, a <= c <= b -> continuity_pt f c) -> exists g : R -> R, continuity g /\ (forall c:R, a <= c <= b -> g c = f c).
proof: Proof. intros; elim H; intro. - set (h := fun x:R => match Rle_dec x a with | left _ => f0 a | right _ => match Rle_dec x b with | left _ => f0 x | right _ => f0 b end end). assert (H2 : 0 < b - a). { apply Rlt_0_minus; assumption. } exists h; split. + unfold continuity; intro; case (Rtotal_order x a); intro. * unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; exists (a - x); split. -- change (0 < a - x); apply Rlt_0_minus; assumption. -- intros; elim H5; clear H5; intros _ H5; unfold h. case (Rle_dec x a) as [|[]]. ++ case (Rle_dec x0 a) as [|[]]. ** unfold Rminus; rewrite Rplus_opp_r, Rabs_R0; assumption. ** left; apply Rplus_lt_reg_l with (- x); do 2 rewrite (Rplus_comm (- x)); apply Rle_lt_trans with (Rabs (x0 - x)). { apply RRle_abs. } assumption. ++ left; assumption. * elim H3; intro. -- assert (H5 : a <= a <= b). { split; [ right; reflexivity | left; assumption ]. } assert (H6 := H0 _ H5); unfold continuity_pt in H6; unfold continue_in in H6; unfold limit1_in in H6; unfold limit_in in H6; simpl in H6; unfold Rdist in H6; unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; elim (H6 _ H7); intros; exists (Rmin x0 (b - a)); split. ++ unfold Rmin; case (Rle_dec x0 (b - a)); intro. ** elim H8; intros; assumption. ** change (0 < b - a); apply Rlt_0_minus; assumption. ++ intros; elim H9; clear H9; intros _ H9; cut (x1 < b). ** intro; unfold h; case (Rle_dec x a) as [|[]]. { case (Rle_dec x1 a) as [Hlta|Hnlea]. - unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. - case (Rle_dec x1 b) as [Hleb|[]]. + elim H8; intros; apply H12; split. * unfold D_x, no_cond; split. -- trivial. -- red; intro; elim Hnlea; right; symmetry ; assumption. * apply Rlt_le_trans with (Rmin x0 (b - a)). -- rewrite H4 in H9; apply H9. -- apply Rmin_l. + left; assumption. } right; assumption. ** apply Rplus_lt_reg_l with (- a); do 2 rewrite (Rplus_comm (- a)); rewrite H4 in H9; apply Rle_lt_trans with (Rabs (x1 - a)). { apply RRle_abs. } apply Rlt_le_trans with (Rmin x0 (b - a)). { assumption. } apply Rmin_r. -- case (Rtotal_order x b); intro. ++ assert (H6 : a <= x <= b). { split; left; assumption. } assert (H7 := H0 _ H6); unfold continuity_pt in H7; unfold continue_in in H7; unfold limit1_in in H7; unfold limit_in in H7; simpl in H7; unfold Rdist in H7; unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; elim (H7 _ H8); intros; elim H9; clear H9; intros. assert (H11 : 0 < x - a). { apply Rlt_0_minus; assumption. } assert (H12 : 0 < b - x). { apply Rlt_0_minus; assumption. } exists (Rmin x0 (Rmin (x - a) (b - x))); split. ** unfold Rmin; case (Rle_dec (x - a) (b - x)) as [Hle|Hnle]. { case (Rle_dec x0 (x - a)) as [Hlea|Hnlea]; assumption. } case (Rle_dec x0 (b - x)) as [Hleb|Hnleb]; assumption. ** intros x1 (H13,H14); cut (a < x1 < b). { intro; elim H15; clear H15; intros; unfold h; case (Rle_dec x a) as [Hle|Hnle]. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle H4)). - case (Rle_dec x b) as [|[]]. + case (Rle_dec x1 a) as [Hle0|]. * elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle0 H15)). * case (Rle_dec x1 b) as [|[]]. -- apply H10; split. ++ assumption. ++ apply Rlt_le_trans with (Rmin x0 (Rmin (x - a) (b - x))). ** assumption. ** apply Rmin_l. -- left; assumption. + left; assumption. } split. { apply Ropp_lt_cancel; apply Rplus_lt_reg_l with x; apply Rle_lt_trans with (Rabs (x1 - x)). - rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs. - apply Rlt_le_trans with (Rmin x0 (Rmin (x - a) (b - x))). + assumption. + apply Rle_trans with (Rmin (x - a) (b - x)). * apply Rmin_r. * apply Rmin_l. } apply Rplus_lt_reg_l with (- x); do 2 rewrite (Rplus_comm (- x)); apply Rle_lt_trans with (Rabs (x1 - x)). { apply RRle_abs. } apply Rlt_le_trans with (Rmin x0 (Rmin (x - a) (b - x))). { assumption. } apply Rle_trans with (Rmin (x - a) (b - x)); apply Rmin_r. ++ elim H5; intro. ** assert (H7 : a <= b <= b). { split; [ left; assumption | right; reflexivity ]. } assert (H8 := H0 _ H7); unfold continuity_pt in H8; unfold continue_in in H8; unfold limit1_in in H8; unfold limit_in in H8; simpl in H8; unfold Rdist in H8; unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; elim (H8 _ H9); intros; exists (Rmin x0 (b - a)); split. { unfold Rmin; case (Rle_dec x0 (b - a)); intro. - elim H10; intros; assumption. - change (0 < b - a); apply Rlt_0_minus; assumption. } intros; elim H11; clear H11; intros _ H11; cut (a < x1). { intro; unfold h; case (Rle_dec x a) as [Hlea|Hnlea]. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hlea H4)). - case (Rle_dec x1 a) as [Hlea'|Hnlea']. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hlea' H12)). + case (Rle_dec x b) as [Hleb|Hnleb]. * case (Rle_dec x1 b) as [Hleb'|Hnleb']. -- rewrite H6; elim H10; intros; destruct Hleb'. ++ apply H14; split. ** unfold D_x, no_cond; split. { trivial. } red; intro; rewrite <- H16 in H15; elim (Rlt_irrefl _ H15). ** rewrite H6 in H11; apply Rlt_le_trans with (Rmin x0 (b - a)). { apply H11. } apply Rmin_l. ++ rewrite H15; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. -- rewrite H6; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. * elim Hnleb; right; assumption. } rewrite H6 in H11; apply Ropp_lt_cancel; apply Rplus_lt_reg_l with b; apply Rle_lt_trans with (Rabs (x1 - b)). { rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs. } apply Rlt_le_trans with (Rmin x0 (b - a)). { assumption. } apply Rmin_r. ** unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; exists (x - b); split. { change (0 < x - b); apply Rlt_0_minus; assumption. } intros; elim H8; clear H8; intros. assert (H10 : b < x0). { apply Ropp_lt_cancel; apply Rplus_lt_reg_l with x; apply Rle_lt_trans with (Rabs (x0 - x)). - rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs. - assumption. } unfold h; case (Rle_dec x a) as [Hle|Hnle]. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle H4)). } case (Rle_dec x b) as [Hleb|Hnleb]. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hleb H6)). } case (Rle_dec x0 a) as [Hlea'|Hnlea']. { elim (Rlt_irrefl _ (Rlt_trans _ _ _ H1 (Rlt_le_trans _ _ _ H10 Hlea'))). } case (Rle_dec x0 b) as [Hleb'|Hnleb']. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hleb' H10)). } unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + intros; elim H3; intros; unfold h; case (Rle_dec c a) as [[|]|]. * elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 H6)). * rewrite H6; reflexivity. * case (Rle_dec c b) as [|[]]. -- reflexivity. -- assumption. - exists (fun _:R => f0 a); split. + apply derivable_continuous; apply (derivable_const (f0 a)). + intros; elim H2; intros; rewrite H1 in H3; cut (b = c). * intro; rewrite <- H5; rewrite H1; reflexivity. * apply Rle_antisym; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type