proposition: Lemma continuity_ab_maj : forall (f:R -> R) (a b:R), a <= b -> (forall c:R, a <= c <= b -> continuity_pt f c) -> exists Mx : R, (forall c:R, a <= c <= b -> f c <= f Mx) /\ a <= Mx <= b.
proof: Proof. intros; cut (exists g : R -> R, continuity g /\ (forall c:R, a <= c <= b -> g c = f0 c)). - intro HypProl. elim HypProl; intros g Hcont_eq. elim Hcont_eq; clear Hcont_eq; intros Hcont Heq. assert (H1 := compact_P3 a b). assert (H2 := continuity_compact g (fun c:R => a <= c <= b) Hcont H1). assert (H3 := compact_P2 _ H2). assert (H4 := compact_P1 _ H2). cut (bound (image_dir g (fun c:R => a <= c <= b))). 1:cut (exists x : R, image_dir g (fun c:R => a <= c <= b) x). + intros; assert (H7 := completeness _ H6 H5). elim H7; clear H7; intros M H7; cut (image_dir g (fun c:R => a <= c <= b) M). * intro; unfold image_dir in H8; elim H8; clear H8; intros Mxx H8; elim H8; clear H8; intros; exists Mxx; split. -- intros; rewrite <- (Heq c H10); rewrite <- (Heq Mxx H9); intros; rewrite <- H8; unfold is_lub in H7; elim H7; clear H7; intros H7 _; unfold is_upper_bound in H7; apply H7; unfold image_dir; exists c; split; [ reflexivity | apply H10 ]. -- apply H9. * elim (classic (image_dir g (fun c:R => a <= c <= b) M)); intro. -- assumption. -- cut (exists eps : posreal, (forall y:R, ~ intersection_domain (disc M eps) (image_dir g (fun c:R => a <= c <= b)) y)). { intro; elim H9; clear H9; intros eps H9; unfold is_lub in H7; elim H7; clear H7; intros; cut (is_upper_bound (image_dir g (fun c:R => a <= c <= b)) (M - eps)). - intro; assert (H12 := H10 _ H11); cut (M - eps < M). + intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H12 H13)). + pattern M at 2; rewrite <- Rplus_0_r; unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_0; rewrite Ropp_involutive; apply (cond_pos eps). - unfold is_upper_bound, image_dir; intros; cut (x <= M). + intro; destruct (Rle_dec x (M - eps)) as [H13|]. * apply H13. * elim (H9 x); unfold intersection_domain, disc, image_dir; split. -- rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; rewrite Rabs_right. ++ apply Rplus_lt_reg_l with (x - eps); replace (x - eps + (M - x)) with (M - eps) by ring. replace (x - eps + eps) with x by ring. auto with real. ++ apply Rge_minus; apply Rle_ge; apply H12. -- apply H11. + apply H7; apply H11. } cut (exists V : R -> Prop, neighbourhood V M /\ (forall y:R, ~ intersection_domain V (image_dir g (fun c:R => a <= c <= b)) y)). { intro; elim H9; intros V H10; elim H10; clear H10; intros. unfold neighbourhood in H10; elim H10; intros del H12; exists del; intros; red; intro; elim (H11 y). unfold intersection_domain; unfold intersection_domain in H13; elim H13; clear H13; intros; split. - apply (H12 _ H13). - apply H14. } cut (~ point_adherent (image_dir g (fun c:R => a <= c <= b)) M). { intro; unfold point_adherent in H9. assert (H10 := not_all_ex_not _ (fun V:R -> Prop => neighbourhood V M -> exists y : R, intersection_domain V (image_dir g (fun c:R => a <= c <= b)) y) H9). elim H10; intros V0 H11; exists V0; assert (H12 := imply_to_and _ _ H11); elim H12; clear H12; intros. split. - apply H12. - apply (not_ex_all_not _ _ H13). } red; intro; cut (adherence (image_dir g (fun c:R => a <= c <= b)) M). ++ intro; elim (closed_set_P1 (image_dir g (fun c:R => a <= c <= b))); intros H11 _; assert (H12 := H11 H3). elim H8. unfold eq_Dom in H12; elim H12; clear H12; intros. apply (H13 _ H10). ++ apply H9. + exists (g a); unfold image_dir; exists a; split. * reflexivity. * split; [ right; reflexivity | apply H ]. + unfold bound; unfold bounded in H4; elim H4; clear H4; intros m H4; elim H4; clear H4; intros M H4; exists M; unfold is_upper_bound; intros; elim (H4 _ H5); intros _ H6; apply H6. - apply prolongement_C0; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type