diff options
Diffstat (limited to 'theories/Reals/Rtopology.v')
| -rw-r--r-- | theories/Reals/Rtopology.v | 3175 |
1 files changed, 1611 insertions, 1564 deletions
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 84f3b081..aa47d72f 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -5,8 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -(*i $Id: Rtopology.v 5920 2004-07-16 20:01:26Z herbelin $ i*) + +(*i $Id: Rtopology.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -15,10 +15,13 @@ Require Import RList. Require Import Classical_Prop. Require Import Classical_Pred_Type. Open Local Scope R_scope. + +(** * General definitions and propositions *) + Definition included (D1 D2:R -> Prop) : Prop := forall x:R, D1 x -> D2 x. Definition disc (x:R) (delta:posreal) (y:R) : Prop := Rabs (y - x) < delta. Definition neighbourhood (V:R -> Prop) (x:R) : Prop := - exists delta : posreal, included (disc x delta) V. + exists delta : posreal, included (disc x delta) V. Definition open_set (D:R -> Prop) : Prop := forall x:R, D x -> neighbourhood D x. Definition complementary (D:R -> Prop) (c:R) : Prop := ~ D c. @@ -28,15 +31,17 @@ Definition union_domain (D1 D2:R -> Prop) (c:R) : Prop := D1 c \/ D2 c. Definition interior (D:R -> Prop) (x:R) : Prop := neighbourhood D x. Lemma interior_P1 : forall D:R -> Prop, included (interior D) D. -intros; unfold included in |- *; unfold interior in |- *; intros; - unfold neighbourhood in H; elim H; intros; unfold included in H0; - apply H0; unfold disc in |- *; unfold Rminus in |- *; - rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos x0). +Proof. + intros; unfold included in |- *; unfold interior in |- *; intros; + unfold neighbourhood in H; elim H; intros; unfold included in H0; + apply H0; unfold disc in |- *; unfold Rminus in |- *; + rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos x0). Qed. Lemma interior_P2 : forall D:R -> Prop, open_set D -> included D (interior D). -intros; unfold open_set in H; unfold included in |- *; intros; - assert (H1 := H _ H0); unfold interior in |- *; apply H1. +Proof. + intros; unfold open_set in H; unfold included in |- *; intros; + assert (H1 := H _ H0); unfold interior in |- *; apply H1. Qed. Definition point_adherent (D:R -> Prop) (x:R) : Prop := @@ -45,94 +50,100 @@ Definition point_adherent (D:R -> Prop) (x:R) : Prop := Definition adherence (D:R -> Prop) (x:R) : Prop := point_adherent D x. Lemma adherence_P1 : forall D:R -> Prop, included D (adherence D). -intro; unfold included in |- *; intros; unfold adherence in |- *; - unfold point_adherent in |- *; intros; exists x; - unfold intersection_domain in |- *; split. -unfold neighbourhood in H0; elim H0; intros; unfold included in H1; apply H1; - unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; - rewrite Rabs_R0; apply (cond_pos x0). -apply H. +Proof. + intro; unfold included in |- *; intros; unfold adherence in |- *; + unfold point_adherent in |- *; intros; exists x; + unfold intersection_domain in |- *; split. + unfold neighbourhood in H0; elim H0; intros; unfold included in H1; apply H1; + unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; + rewrite Rabs_R0; apply (cond_pos x0). + apply H. Qed. Lemma included_trans : - forall D1 D2 D3:R -> Prop, - included D1 D2 -> included D2 D3 -> included D1 D3. -unfold included in |- *; intros; apply H0; apply H; apply H1. + forall D1 D2 D3:R -> Prop, + included D1 D2 -> included D2 D3 -> included D1 D3. +Proof. + unfold included in |- *; intros; apply H0; apply H; apply H1. Qed. Lemma interior_P3 : forall D:R -> Prop, open_set (interior D). -intro; unfold open_set, interior in |- *; unfold neighbourhood in |- *; - intros; elim H; intros. -exists x0; unfold included in |- *; intros. -set (del := x0 - Rabs (x - x1)). -cut (0 < del). -intro; exists (mkposreal del H2); intros. -cut (included (disc x1 (mkposreal del H2)) (disc x x0)). -intro; assert (H5 := included_trans _ _ _ H4 H0). -apply H5; apply H3. -unfold included in |- *; unfold disc in |- *; intros. -apply Rle_lt_trans with (Rabs (x3 - x1) + Rabs (x1 - x)). -replace (x3 - x) with (x3 - x1 + (x1 - x)); [ apply Rabs_triang | ring ]. -replace (pos x0) with (del + Rabs (x1 - x)). -do 2 rewrite <- (Rplus_comm (Rabs (x1 - x))); apply Rplus_lt_compat_l; - apply H4. -unfold del in |- *; rewrite <- (Rabs_Ropp (x - x1)); rewrite Ropp_minus_distr; - ring. -unfold del in |- *; apply Rplus_lt_reg_r with (Rabs (x - x1)); - rewrite Rplus_0_r; - replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0); - [ idtac | ring ]. -unfold disc in H1; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1. +Proof. + intro; unfold open_set, interior in |- *; unfold neighbourhood in |- *; + intros; elim H; intros. + exists x0; unfold included in |- *; intros. + set (del := x0 - Rabs (x - x1)). + cut (0 < del). + intro; exists (mkposreal del H2); intros. + cut (included (disc x1 (mkposreal del H2)) (disc x x0)). + intro; assert (H5 := included_trans _ _ _ H4 H0). + apply H5; apply H3. + unfold included in |- *; unfold disc in |- *; intros. + apply Rle_lt_trans with (Rabs (x3 - x1) + Rabs (x1 - x)). + replace (x3 - x) with (x3 - x1 + (x1 - x)); [ apply Rabs_triang | ring ]. + replace (pos x0) with (del + Rabs (x1 - x)). + do 2 rewrite <- (Rplus_comm (Rabs (x1 - x))); apply Rplus_lt_compat_l; + apply H4. + unfold del in |- *; rewrite <- (Rabs_Ropp (x - x1)); rewrite Ropp_minus_distr; + ring. + unfold del in |- *; apply Rplus_lt_reg_r with (Rabs (x - x1)); + rewrite Rplus_0_r; + replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0); + [ idtac | ring ]. + unfold disc in H1; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1. Qed. Lemma complementary_P1 : - forall D:R -> Prop, - ~ (exists y : R, intersection_domain D (complementary D) y). -intro; red in |- *; intro; elim H; intros; - unfold intersection_domain, complementary in H0; elim H0; - intros; elim H2; assumption. + forall D:R -> Prop, + ~ (exists y : R, intersection_domain D (complementary D) y). +Proof. + intro; red in |- *; intro; elim H; intros; + unfold intersection_domain, complementary in H0; elim H0; + intros; elim H2; assumption. Qed. Lemma adherence_P2 : - forall D:R -> Prop, closed_set D -> included (adherence D) D. -unfold closed_set in |- *; unfold open_set, complementary in |- *; intros; - unfold included, adherence in |- *; intros; assert (H1 := classic (D x)); - elim H1; intro. -assumption. -assert (H3 := H _ H2); assert (H4 := H0 _ H3); elim H4; intros; - unfold intersection_domain in H5; elim H5; intros; - elim H6; assumption. + forall D:R -> Prop, closed_set D -> included (adherence D) D. +Proof. + unfold closed_set in |- *; unfold open_set, complementary in |- *; intros; + unfold included, adherence in |- *; intros; assert (H1 := classic (D x)); + elim H1; intro. + assumption. + assert (H3 := H _ H2); assert (H4 := H0 _ H3); elim H4; intros; + unfold intersection_domain in H5; elim H5; intros; + elim H6; assumption. Qed. Lemma adherence_P3 : forall D:R -> Prop, closed_set (adherence D). -intro; unfold closed_set, adherence in |- *; - unfold open_set, complementary, point_adherent in |- *; - intros; - set - (P := - fun V:R -> Prop => - neighbourhood V x -> exists y : R, intersection_domain V D y); - assert (H0 := not_all_ex_not _ P H); elim H0; intros V0 H1; - unfold P in H1; assert (H2 := imply_to_and _ _ H1); - unfold neighbourhood in |- *; elim H2; intros; unfold neighbourhood in H3; - elim H3; intros; exists x0; unfold included in |- *; - intros; red in |- *; intro. -assert (H8 := H7 V0); - cut (exists delta : posreal, (forall x:R, disc x1 delta x -> V0 x)). -intro; assert (H10 := H8 H9); elim H4; assumption. -cut (0 < x0 - Rabs (x - x1)). -intro; set (del := mkposreal _ H9); exists del; intros; - unfold included in H5; apply H5; unfold disc in |- *; - apply Rle_lt_trans with (Rabs (x2 - x1) + Rabs (x1 - x)). -replace (x2 - x) with (x2 - x1 + (x1 - x)); [ apply Rabs_triang | ring ]. -replace (pos x0) with (del + Rabs (x1 - x)). -do 2 rewrite <- (Rplus_comm (Rabs (x1 - x))); apply Rplus_lt_compat_l; - apply H10. -unfold del in |- *; simpl in |- *; rewrite <- (Rabs_Ropp (x - x1)); - rewrite Ropp_minus_distr; ring. -apply Rplus_lt_reg_r with (Rabs (x - x1)); rewrite Rplus_0_r; - replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0); - [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H6 | ring ]. +Proof. + intro; unfold closed_set, adherence in |- *; + unfold open_set, complementary, point_adherent in |- *; + intros; + set + (P := + fun V:R -> Prop => + neighbourhood V x -> exists y : R, intersection_domain V D y); + assert (H0 := not_all_ex_not _ P H); elim H0; intros V0 H1; + unfold P in H1; assert (H2 := imply_to_and _ _ H1); + unfold neighbourhood in |- *; elim H2; intros; unfold neighbourhood in H3; + elim H3; intros; exists x0; unfold included in |- *; + intros; red in |- *; intro. + assert (H8 := H7 V0); + cut (exists delta : posreal, (forall x:R, disc x1 delta x -> V0 x)). + intro; assert (H10 := H8 H9); elim H4; assumption. + cut (0 < x0 - Rabs (x - x1)). + intro; set (del := mkposreal _ H9); exists del; intros; + unfold included in H5; apply H5; unfold disc in |- *; + apply Rle_lt_trans with (Rabs (x2 - x1) + Rabs (x1 - x)). + replace (x2 - x) with (x2 - x1 + (x1 - x)); [ apply Rabs_triang | ring ]. + replace (pos x0) with (del + Rabs (x1 - x)). + do 2 rewrite <- (Rplus_comm (Rabs (x1 - x))); apply Rplus_lt_compat_l; + apply H10. + unfold del in |- *; simpl in |- *; rewrite <- (Rabs_Ropp (x - x1)); + rewrite Ropp_minus_distr; ring. + apply Rplus_lt_reg_r with (Rabs (x - x1)); rewrite Rplus_0_r; + replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0); + [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H6 | ring ]. Qed. Definition eq_Dom (D1 D2:R -> Prop) : Prop := @@ -141,231 +152,243 @@ Definition eq_Dom (D1 D2:R -> Prop) : Prop := Infix "=_D" := eq_Dom (at level 70, no associativity). Lemma open_set_P1 : forall D:R -> Prop, open_set D <-> D =_D interior D. -intro; split. -intro; unfold eq_Dom in |- *; split. -apply interior_P2; assumption. -apply interior_P1. -intro; unfold eq_Dom in H; elim H; clear H; intros; unfold open_set in |- *; - intros; unfold included, interior in H; unfold included in H0; - apply (H _ H1). +Proof. + intro; split. + intro; unfold eq_Dom in |- *; split. + apply interior_P2; assumption. + apply interior_P1. + intro; unfold eq_Dom in H; elim H; clear H; intros; unfold open_set in |- *; + intros; unfold included, interior in H; unfold included in H0; + apply (H _ H1). Qed. Lemma closed_set_P1 : forall D:R -> Prop, closed_set D <-> D =_D adherence D. -intro; split. -intro; unfold eq_Dom in |- *; split. -apply adherence_P1. -apply adherence_P2; assumption. -unfold eq_Dom in |- *; unfold included in |- *; intros; - assert (H0 := adherence_P3 D); unfold closed_set in H0; - unfold closed_set in |- *; unfold open_set in |- *; - unfold open_set in H0; intros; assert (H2 : complementary (adherence D) x). -unfold complementary in |- *; unfold complementary in H1; red in |- *; intro; - elim H; clear H; intros _ H; elim H1; apply (H _ H2). -assert (H3 := H0 _ H2); unfold neighbourhood in |- *; - unfold neighbourhood in H3; elim H3; intros; exists x0; - unfold included in |- *; unfold included in H4; intros; - assert (H6 := H4 _ H5); unfold complementary in H6; - unfold complementary in |- *; red in |- *; intro; - elim H; clear H; intros H _; elim H6; apply (H _ H7). +Proof. + intro; split. + intro; unfold eq_Dom in |- *; split. + apply adherence_P1. + apply adherence_P2; assumption. + unfold eq_Dom in |- *; unfold included in |- *; intros; + assert (H0 := adherence_P3 D); unfold closed_set in H0; + unfold closed_set in |- *; unfold open_set in |- *; + unfold open_set in H0; intros; assert (H2 : complementary (adherence D) x). + unfold complementary in |- *; unfold complementary in H1; red in |- *; intro; + elim H; clear H; intros _ H; elim H1; apply (H _ H2). + assert (H3 := H0 _ H2); unfold neighbourhood in |- *; + unfold neighbourhood in H3; elim H3; intros; exists x0; + unfold included in |- *; unfold included in H4; intros; + assert (H6 := H4 _ H5); unfold complementary in H6; + unfold complementary in |- *; red in |- *; intro; + elim H; clear H; intros H _; elim H6; apply (H _ H7). Qed. Lemma neighbourhood_P1 : - forall (D1 D2:R -> Prop) (x:R), - included D1 D2 -> neighbourhood D1 x -> neighbourhood D2 x. -unfold included, neighbourhood in |- *; intros; elim H0; intros; exists x0; - intros; unfold included in |- *; unfold included in H1; - intros; apply (H _ (H1 _ H2)). + forall (D1 D2:R -> Prop) (x:R), + included D1 D2 -> neighbourhood D1 x -> neighbourhood D2 x. +Proof. + unfold included, neighbourhood in |- *; intros; elim H0; intros; exists x0; + intros; unfold included in |- *; unfold included in H1; + intros; apply (H _ (H1 _ H2)). Qed. Lemma open_set_P2 : - forall D1 D2:R -> Prop, - open_set D1 -> open_set D2 -> open_set (union_domain D1 D2). -unfold open_set in |- *; intros; unfold union_domain in H1; elim H1; intro. -apply neighbourhood_P1 with D1. -unfold included, union_domain in |- *; tauto. -apply H; assumption. -apply neighbourhood_P1 with D2. -unfold included, union_domain in |- *; tauto. -apply H0; assumption. + forall D1 D2:R -> Prop, + open_set D1 -> open_set D2 -> open_set (union_domain D1 D2). +Proof. + unfold open_set in |- *; intros; unfold union_domain in H1; elim H1; intro. + apply neighbourhood_P1 with D1. + unfold included, union_domain in |- *; tauto. + apply H; assumption. + apply neighbourhood_P1 with D2. + unfold included, union_domain in |- *; tauto. + apply H0; assumption. Qed. Lemma open_set_P3 : - forall D1 D2:R -> Prop, - open_set D1 -> open_set D2 -> open_set (intersection_domain D1 D2). -unfold open_set in |- *; intros; unfold intersection_domain in H1; elim H1; - intros. -assert (H4 := H _ H2); assert (H5 := H0 _ H3); - unfold intersection_domain in |- *; unfold neighbourhood in H4, H5; - elim H4; clear H; intros del1 H; elim H5; clear H0; - intros del2 H0; cut (0 < Rmin del1 del2). -intro; set (del := mkposreal _ H6). -exists del; unfold included in |- *; intros; unfold included in H, H0; - unfold disc in H, H0, H7. -split. -apply H; apply Rlt_le_trans with (pos del). -apply H7. -unfold del in |- *; simpl in |- *; apply Rmin_l. -apply H0; apply Rlt_le_trans with (pos del). -apply H7. -unfold del in |- *; simpl in |- *; apply Rmin_r. -unfold Rmin in |- *; case (Rle_dec del1 del2); intro. -apply (cond_pos del1). -apply (cond_pos del2). + forall D1 D2:R -> Prop, + open_set D1 -> open_set D2 -> open_set (intersection_domain D1 D2). +Proof. + unfold open_set in |- *; intros; unfold intersection_domain in H1; elim H1; + intros. + assert (H4 := H _ H2); assert (H5 := H0 _ H3); + unfold intersection_domain in |- *; unfold neighbourhood in H4, H5; + elim H4; clear H; intros del1 H; elim H5; clear H0; + intros del2 H0; cut (0 < Rmin del1 del2). + intro; set (del := mkposreal _ H6). + exists del; unfold included in |- *; intros; unfold included in H, H0; + unfold disc in H, H0, H7. + split. + apply H; apply Rlt_le_trans with (pos del). + apply H7. + unfold del in |- *; simpl in |- *; apply Rmin_l. + apply H0; apply Rlt_le_trans with (pos del). + apply H7. + unfold del in |- *; simpl in |- *; apply Rmin_r. + unfold Rmin in |- *; case (Rle_dec del1 del2); intro. + apply (cond_pos del1). + apply (cond_pos del2). Qed. Lemma open_set_P4 : open_set (fun x:R => False). -unfold open_set in |- *; intros; elim H. +Proof. + unfold open_set in |- *; intros; elim H. Qed. Lemma open_set_P5 : open_set (fun x:R => True). -unfold open_set in |- *; intros; unfold neighbourhood in |- *. -exists (mkposreal 1 Rlt_0_1); unfold included in |- *; intros; trivial. +Proof. + unfold open_set in |- *; intros; unfold neighbourhood in |- *. + exists (mkposreal 1 Rlt_0_1); unfold included in |- *; intros; trivial. Qed. Lemma disc_P1 : forall (x:R) (del:posreal), open_set (disc x del). -intros; assert (H := open_set_P1 (disc x del)). -elim H; intros; apply H1. -unfold eq_Dom in |- *; split. -unfold included, interior, disc in |- *; intros; - cut (0 < del - Rabs (x - x0)). -intro; set (del2 := mkposreal _ H3). -exists del2; unfold included in |- *; intros. -apply Rle_lt_trans with (Rabs (x1 - x0) + Rabs (x0 - x)). -replace (x1 - x) with (x1 - x0 + (x0 - x)); [ apply Rabs_triang | ring ]. -replace (pos del) with (del2 + Rabs (x0 - x)). -do 2 rewrite <- (Rplus_comm (Rabs (x0 - x))); apply Rplus_lt_compat_l. -apply H4. -unfold del2 in |- *; simpl in |- *; rewrite <- (Rabs_Ropp (x - x0)); - rewrite Ropp_minus_distr; ring. -apply Rplus_lt_reg_r with (Rabs (x - x0)); rewrite Rplus_0_r; - replace (Rabs (x - x0) + (del - Rabs (x - x0))) with (pos del); - [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2 | ring ]. -apply interior_P1. +Proof. + intros; assert (H := open_set_P1 (disc x del)). + elim H; intros; apply H1. + unfold eq_Dom in |- *; split. + unfold included, interior, disc in |- *; intros; + cut (0 < del - Rabs (x - x0)). + intro; set (del2 := mkposreal _ H3). + exists del2; unfold included in |- *; intros. + apply Rle_lt_trans with (Rabs (x1 - x0) + Rabs (x0 - x)). + replace (x1 - x) with (x1 - x0 + (x0 - x)); [ apply Rabs_triang | ring ]. + replace (pos del) with (del2 + Rabs (x0 - x)). + do 2 rewrite <- (Rplus_comm (Rabs (x0 - x))); apply Rplus_lt_compat_l. + apply H4. + unfold del2 in |- *; simpl in |- *; rewrite <- (Rabs_Ropp (x - x0)); + rewrite Ropp_minus_distr; ring. + apply Rplus_lt_reg_r with (Rabs (x - x0)); rewrite Rplus_0_r; + replace (Rabs (x - x0) + (del - Rabs (x - x0))) with (pos del); + [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2 | ring ]. + apply interior_P1. Qed. Lemma continuity_P1 : - forall (f:R -> R) (x:R), - continuity_pt f x <-> - (forall W:R -> Prop, + forall (f:R -> R) (x:R), + continuity_pt f x <-> + (forall W:R -> Prop, neighbourhood W (f x) -> - exists V : R -> Prop, + exists V : R -> Prop, neighbourhood V x /\ (forall y:R, V y -> W (f y))). -intros; split. -intros; unfold neighbourhood in H0. -elim H0; intros del1 H1. -unfold continuity_pt in H; unfold continue_in in H; unfold limit1_in in H; - unfold limit_in in H; simpl in H; unfold R_dist in H. -assert (H2 := H del1 (cond_pos del1)). -elim H2; intros del2 H3. -elim H3; intros. -exists (disc x (mkposreal del2 H4)). -intros; unfold included in H1; split. -unfold neighbourhood, disc in |- *. -exists (mkposreal del2 H4). -unfold included in |- *; intros; assumption. -intros; apply H1; unfold disc in |- *; case (Req_dec y x); intro. -rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; - apply (cond_pos del1). -apply H5; split. -unfold D_x, no_cond in |- *; split. -trivial. -apply (sym_not_eq (A:=R)); apply H7. -unfold disc in H6; apply H6. -intros; unfold continuity_pt in |- *; unfold continue_in in |- *; - unfold limit1_in in |- *; unfold limit_in in |- *; - intros. -assert (H1 := H (disc (f x) (mkposreal eps H0))). -cut (neighbourhood (disc (f x) (mkposreal eps H0)) (f x)). -intro; assert (H3 := H1 H2). -elim H3; intros D H4; elim H4; intros; unfold neighbourhood in H5; elim H5; - intros del1 H7. -exists (pos del1); split. -apply (cond_pos del1). -intros; elim H8; intros; simpl in H10; unfold R_dist in H10; simpl in |- *; - unfold R_dist in |- *; apply (H6 _ (H7 _ H10)). -unfold neighbourhood, disc in |- *; exists (mkposreal eps H0); - unfold included in |- *; intros; assumption. +Proof. + intros; split. + intros; unfold neighbourhood in H0. + elim H0; intros del1 H1. + unfold continuity_pt in H; unfold continue_in in H; unfold limit1_in in H; + unfold limit_in in H; simpl in H; unfold R_dist in H. + assert (H2 := H del1 (cond_pos del1)). + elim H2; intros del2 H3. + elim H3; intros. + exists (disc x (mkposreal del2 H4)). + intros; unfold included in H1; split. + unfold neighbourhood, disc in |- *. + exists (mkposreal del2 H4). + unfold included in |- *; intros; assumption. + intros; apply H1; unfold disc in |- *; case (Req_dec y x); intro. + rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + apply (cond_pos del1). + apply H5; split. + unfold D_x, no_cond in |- *; split. + trivial. + apply (sym_not_eq (A:=R)); apply H7. + unfold disc in H6; apply H6. + intros; unfold continuity_pt in |- *; unfold continue_in in |- *; + unfold limit1_in in |- *; unfold limit_in in |- *; + intros. + assert (H1 := H (disc (f x) (mkposreal eps H0))). + cut (neighbourhood (disc (f x) (mkposreal eps H0)) (f x)). + intro; assert (H3 := H1 H2). + elim H3; intros D H4; elim H4; intros; unfold neighbourhood in H5; elim H5; + intros del1 H7. + exists (pos del1); split. + apply (cond_pos del1). + intros; elim H8; intros; simpl in H10; unfold R_dist in H10; simpl in |- *; + unfold R_dist in |- *; apply (H6 _ (H7 _ H10)). + unfold neighbourhood, disc in |- *; exists (mkposreal eps H0); + unfold included in |- *; intros; assumption. Qed. Definition image_rec (f:R -> R) (D:R -> Prop) (x:R) : Prop := D (f x). (**********) Lemma continuity_P2 : - forall (f:R -> R) (D:R -> Prop), - continuity f -> open_set D -> open_set (image_rec f D). -intros; unfold open_set in H0; unfold open_set in |- *; intros; - assert (H2 := continuity_P1 f x); elim H2; intros H3 _; - assert (H4 := H3 (H x)); unfold neighbourhood, image_rec in |- *; - unfold image_rec in H1; assert (H5 := H4 D (H0 (f x) H1)); - elim H5; intros V0 H6; elim H6; intros; unfold neighbourhood in H7; - elim H7; intros del H9; exists del; unfold included in H9; - unfold included in |- *; intros; apply (H8 _ (H9 _ H10)). + forall (f:R -> R) (D:R -> Prop), + continuity f -> open_set D -> open_set (image_rec f D). +Proof. + intros; unfold open_set in H0; unfold open_set in |- *; intros; + assert (H2 := continuity_P1 f x); elim H2; intros H3 _; + assert (H4 := H3 (H x)); unfold neighbourhood, image_rec in |- *; + unfold image_rec in H1; assert (H5 := H4 D (H0 (f x) H1)); + elim H5; intros V0 H6; elim H6; intros; unfold neighbourhood in H7; + elim H7; intros del H9; exists del; unfold included in H9; + unfold included in |- *; intros; apply (H8 _ (H9 _ H10)). Qed. (**********) Lemma continuity_P3 : - forall f:R -> R, - continuity f <-> - (forall D:R -> Prop, open_set D -> open_set (image_rec f D)). -intros; split. -intros; apply continuity_P2; assumption. -intros; unfold continuity in |- *; unfold continuity_pt in |- *; - unfold continue_in in |- *; unfold limit1_in in |- *; - unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; - intros; cut (open_set (disc (f x) (mkposreal _ H0))). -intro; assert (H2 := H _ H1). -unfold open_set, image_rec in H2; cut (disc (f x) (mkposreal _ H0) (f x)). -intro; assert (H4 := H2 _ H3). -unfold neighbourhood in H4; elim H4; intros del H5. -exists (pos del); split. -apply (cond_pos del). -intros; unfold included in H5; apply H5; elim H6; intros; apply H8. -unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; - rewrite Rabs_R0; apply H0. -apply disc_P1. + forall f:R -> R, + continuity f <-> + (forall D:R -> Prop, open_set D -> open_set (image_rec f D)). +Proof. + intros; split. + intros; apply continuity_P2; assumption. + intros; unfold continuity in |- *; unfold continuity_pt in |- *; + unfold continue_in in |- *; unfold limit1_in in |- *; + unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; + intros; cut (open_set (disc (f x) (mkposreal _ H0))). + intro; assert (H2 := H _ H1). + unfold open_set, image_rec in H2; cut (disc (f x) (mkposreal _ H0) (f x)). + intro; assert (H4 := H2 _ H3). + unfold neighbourhood in H4; elim H4; intros del H5. + exists (pos del); split. + apply (cond_pos del). + intros; unfold included in H5; apply H5; elim H6; intros; apply H8. + unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; + rewrite Rabs_R0; apply H0. + apply disc_P1. Qed. (**********) Theorem Rsepare : - forall x y:R, - x <> y -> + forall x y:R, + x <> y -> exists V : R -> Prop, - (exists W : R -> Prop, + (exists W : R -> Prop, neighbourhood V x /\ neighbourhood W y /\ ~ (exists y : R, intersection_domain V W y)). -intros x y Hsep; set (D := Rabs (x - y)). -cut (0 < D / 2). -intro; exists (disc x (mkposreal _ H)). -exists (disc y (mkposreal _ H)); split. -unfold neighbourhood in |- *; exists (mkposreal _ H); unfold included in |- *; - tauto. -split. -unfold neighbourhood in |- *; exists (mkposreal _ H); unfold included in |- *; - tauto. -red in |- *; intro; elim H0; intros; unfold intersection_domain in H1; - elim H1; intros. -cut (D < D). -intro; elim (Rlt_irrefl _ H4). -change (Rabs (x - y) < D) in |- *; - apply Rle_lt_trans with (Rabs (x - x0) + Rabs (x0 - y)). -replace (x - y) with (x - x0 + (x0 - y)); [ apply Rabs_triang | ring ]. -rewrite (double_var D); apply Rplus_lt_compat. -rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2. -apply H3. -unfold Rdiv in |- *; apply Rmult_lt_0_compat. -unfold D in |- *; apply Rabs_pos_lt; apply (Rminus_eq_contra _ _ Hsep). -apply Rinv_0_lt_compat; prove_sup0. +Proof. + intros x y Hsep; set (D := Rabs (x - y)). + cut (0 < D / 2). + intro; exists (disc x (mkposreal _ H)). + exists (disc y (mkposreal _ H)); split. + unfold neighbourhood in |- *; exists (mkposreal _ H); unfold included in |- *; + tauto. + split. + unfold neighbourhood in |- *; exists (mkposreal _ H); unfold included in |- *; + tauto. + red in |- *; intro; elim H0; intros; unfold intersection_domain in H1; + elim H1; intros. + cut (D < D). + intro; elim (Rlt_irrefl _ H4). + change (Rabs (x - y) < D) in |- *; + apply Rle_lt_trans with (Rabs (x - x0) + Rabs (x0 - y)). + replace (x - y) with (x - x0 + (x0 - y)); [ apply Rabs_triang | ring ]. + rewrite (double_var D); apply Rplus_lt_compat. + rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2. + apply H3. + unfold Rdiv in |- *; apply Rmult_lt_0_compat. + unfold D in |- *; apply Rabs_pos_lt; apply (Rminus_eq_contra _ _ Hsep). + apply Rinv_0_lt_compat; prove_sup0. Qed. Record family : Type := mkfamily {ind : R -> Prop; - f :> R -> R -> Prop; - cond_fam : forall x:R, (exists y : R, f x y) -> ind x}. + f :> R -> R -> Prop; + cond_fam : forall x:R, (exists y : R, f x y) -> ind x}. Definition family_open_set (f:family) : Prop := forall x:R, open_set (f x). Definition domain_finite (D:R -> Prop) : Prop := - exists l : Rlist, (forall x:R, D x <-> In x l). + exists l : Rlist, (forall x:R, D x <-> In x l). Definition family_finite (f:family) : Prop := domain_finite (ind f). @@ -379,897 +402,913 @@ Definition covering_finite (D:R -> Prop) (f:family) : Prop := covering D f /\ family_finite f. Lemma restriction_family : - forall (f:family) (D:R -> Prop) (x:R), - (exists y : R, (fun z1 z2:R => f z1 z2 /\ D z1) x y) -> - intersection_domain (ind f) D x. -intros; elim H; intros; unfold intersection_domain in |- *; elim H0; intros; - split. -apply (cond_fam f0); exists x0; assumption. -assumption. + forall (f:family) (D:R -> Prop) (x:R), + (exists y : R, (fun z1 z2:R => f z1 z2 /\ D z1) x y) -> + intersection_domain (ind f) D x. +Proof. + intros; elim H; intros; unfold intersection_domain in |- *; elim H0; intros; + split. + apply (cond_fam f0); exists x0; assumption. + assumption. Qed. Definition subfamily (f:family) (D:R -> Prop) : family := mkfamily (intersection_domain (ind f) D) (fun x y:R => f x y /\ D x) - (restriction_family f D). + (restriction_family f D). Definition compact (X:R -> Prop) : Prop := forall f:family, covering_open_set X f -> - exists D : R -> Prop, covering_finite X (subfamily f D). + exists D : R -> Prop, covering_finite X (subfamily f D). (**********) Lemma family_P1 : - forall (f:family) (D:R -> Prop), - family_open_set f -> family_open_set (subfamily f D). -unfold family_open_set in |- *; intros; unfold subfamily in |- *; - simpl in |- *; assert (H0 := classic (D x)). -elim H0; intro. -cut (open_set (f0 x) -> open_set (fun y:R => f0 x y /\ D x)). -intro; apply H2; apply H. -unfold open_set in |- *; unfold neighbourhood in |- *; intros; elim H3; - intros; assert (H6 := H2 _ H4); elim H6; intros; exists x1; - unfold included in |- *; intros; split. -apply (H7 _ H8). -assumption. -cut (open_set (fun y:R => False) -> open_set (fun y:R => f0 x y /\ D x)). -intro; apply H2; apply open_set_P4. -unfold open_set in |- *; unfold neighbourhood in |- *; intros; elim H3; - intros; elim H1; assumption. + forall (f:family) (D:R -> Prop), + family_open_set f -> family_open_set (subfamily f D). +Proof. + unfold family_open_set in |- *; intros; unfold subfamily in |- *; + simpl in |- *; assert (H0 := classic (D x)). + elim H0; intro. + cut (open_set (f0 x) -> open_set (fun y:R => f0 x y /\ D x)). + intro; apply H2; apply H. + unfold open_set in |- *; unfold neighbourhood in |- *; intros; elim H3; + intros; assert (H6 := H2 _ H4); elim H6; intros; exists x1; + unfold included in |- *; intros; split. + apply (H7 _ H8). + assumption. + cut (open_set (fun y:R => False) -> open_set (fun y:R => f0 x y /\ D x)). + intro; apply H2; apply open_set_P4. + unfold open_set in |- *; unfold neighbourhood in |- *; intros; elim H3; + intros; elim H1; assumption. Qed. Definition bounded (D:R -> Prop) : Prop := - exists m : R, (exists M : R, (forall x:R, D x -> m <= x <= M)). + exists m : R, (exists M : R, (forall x:R, D x -> m <= x <= M)). Lemma open_set_P6 : - forall D1 D2:R -> Prop, open_set D1 -> D1 =_D D2 -> open_set D2. -unfold open_set in |- *; unfold neighbourhood in |- *; intros. -unfold eq_Dom in H0; elim H0; intros. -assert (H4 := H _ (H3 _ H1)). -elim H4; intros. -exists x0; apply included_trans with D1; assumption. + forall D1 D2:R -> Prop, open_set D1 -> D1 =_D D2 -> open_set D2. +Proof. + unfold open_set in |- *; unfold neighbourhood in |- *; intros. + unfold eq_Dom in H0; elim H0; intros. + assert (H4 := H _ (H3 _ H1)). + elim H4; intros. + exists x0; apply included_trans with D1; assumption. Qed. (**********) Lemma compact_P1 : forall X:R -> Prop, compact X -> bounded X. -intros; unfold compact in H; set (D := fun x:R => True); - set (g := fun x y:R => Rabs y < x); - cut (forall x:R, (exists y : _, g x y) -> True); - [ intro | intro; trivial ]. -set (f0 := mkfamily D g H0); assert (H1 := H f0); - cut (covering_open_set X f0). -intro; assert (H3 := H1 H2); elim H3; intros D' H4; - unfold covering_finite in H4; elim H4; intros; unfold family_finite in H6; - unfold domain_finite in H6; elim H6; intros l H7; - unfold bounded in |- *; set (r := MaxRlist l). -exists (- r); exists r; intros. -unfold covering in H5; assert (H9 := H5 _ H8); elim H9; intros; - unfold subfamily in H10; simpl in H10; elim H10; intros; - assert (H13 := H7 x0); simpl in H13; cut (intersection_domain D D' x0). -elim H13; clear H13; intros. -assert (H16 := H13 H15); unfold g in H11; split. -cut (x0 <= r). -intro; cut (Rabs x < r). -intro; assert (H19 := Rabs_def2 x r H18); elim H19; intros; left; assumption. -apply Rlt_le_trans with x0; assumption. -apply (MaxRlist_P1 l x0 H16). -cut (x0 <= r). -intro; apply Rle_trans with (Rabs x). -apply RRle_abs. -apply Rle_trans with x0. -left; apply H11. -assumption. -apply (MaxRlist_P1 l x0 H16). -unfold intersection_domain, D in |- *; tauto. -unfold covering_open_set in |- *; split. -unfold covering in |- *; intros; simpl in |- *; exists (Rabs x + 1); - unfold g in |- *; pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; - apply Rplus_lt_compat_l; apply Rlt_0_1. -unfold family_open_set in |- *; intro; case (Rtotal_order 0 x); intro. -apply open_set_P6 with (disc 0 (mkposreal _ H2)). -apply disc_P1. -unfold eq_Dom in |- *; unfold f0 in |- *; simpl in |- *; - unfold g, disc in |- *; split. -unfold included in |- *; intros; unfold Rminus in H3; rewrite Ropp_0 in H3; - rewrite Rplus_0_r in H3; apply H3. -unfold included in |- *; intros; unfold Rminus in |- *; rewrite Ropp_0; - rewrite Rplus_0_r; apply H3. -apply open_set_P6 with (fun x:R => False). -apply open_set_P4. -unfold eq_Dom in |- *; split. -unfold included in |- *; intros; elim H3. -unfold included, f0 in |- *; simpl in |- *; unfold g in |- *; intros; elim H2; - intro; - [ rewrite <- H4 in H3; assert (H5 := Rabs_pos x0); - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H3)) - | assert (H6 := Rabs_pos x0); assert (H7 := Rlt_trans _ _ _ H3 H4); - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7)) ]. +Proof. + intros; unfold compact in H; set (D := fun x:R => True); + set (g := fun x y:R => Rabs y < x); + cut (forall x:R, (exists y : _, g x y) -> True); + [ intro | intro; trivial ]. + set (f0 := mkfamily D g H0); assert (H1 := H f0); + cut (covering_open_set X f0). + intro; assert (H3 := H1 H2); elim H3; intros D' H4; + unfold covering_finite in H4; elim H4; intros; unfold family_finite in H6; + unfold domain_finite in H6; elim H6; intros l H7; + unfold bounded in |- *; set (r := MaxRlist l). + exists (- r); exists r; intros. + unfold covering in H5; assert (H9 := H5 _ H8); elim H9; intros; + unfold subfamily in H10; simpl in H10; elim H10; intros; + assert (H13 := H7 x0); simpl in H13; cut (intersection_domain D D' x0). + elim H13; clear H13; intros. + assert (H16 := H13 H15); unfold g in H11; split. + cut (x0 <= r). + intro; cut (Rabs x < r). + intro; assert (H19 := Rabs_def2 x r H18); elim H19; intros; left; assumption. + apply Rlt_le_trans with x0; assumption. + apply (MaxRlist_P1 l x0 H16). + cut (x0 <= r). + intro; apply Rle_trans with (Rabs x). + apply RRle_abs. + apply Rle_trans with x0. + left; apply H11. + assumption. + apply (MaxRlist_P1 l x0 H16). + unfold intersection_domain, D in |- *; tauto. + unfold covering_open_set in |- *; split. + unfold covering in |- *; intros; simpl in |- *; exists (Rabs x + 1); + unfold g in |- *; pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; + apply Rplus_lt_compat_l; apply Rlt_0_1. + unfold family_open_set in |- *; intro; case (Rtotal_order 0 x); intro. + apply open_set_P6 with (disc 0 (mkposreal _ H2)). + apply disc_P1. + unfold eq_Dom in |- *; unfold f0 in |- *; simpl in |- *; + unfold g, disc in |- *; split. + unfold included in |- *; intros; unfold Rminus in H3; rewrite Ropp_0 in H3; + rewrite Rplus_0_r in H3; apply H3. + unfold included in |- *; intros; unfold Rminus in |- *; rewrite Ropp_0; + rewrite Rplus_0_r; apply H3. + apply open_set_P6 with (fun x:R => False). + apply open_set_P4. + unfold eq_Dom in |- *; split. + unfold included in |- *; intros; elim H3. + unfold included, f0 in |- *; simpl in |- *; unfold g in |- *; intros; elim H2; + intro; + [ rewrite <- H4 in H3; assert (H5 := Rabs_pos x0); + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H3)) + | assert (H6 := Rabs_pos x0); assert (H7 := Rlt_trans _ _ _ H3 H4); + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7)) ]. Qed. (**********) Lemma compact_P2 : forall X:R -> Prop, compact X -> closed_set X. -intros; assert (H0 := closed_set_P1 X); elim H0; clear H0; intros _ H0; - apply H0; clear H0. -unfold eq_Dom in |- *; split. -apply adherence_P1. -unfold included in |- *; unfold adherence in |- *; - unfold point_adherent in |- *; intros; unfold compact in H; - assert (H1 := classic (X x)); elim H1; clear H1; intro. -assumption. -cut (forall y:R, X y -> 0 < Rabs (y - x) / 2). -intro; set (D := X); - set (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y); - cut (forall x:R, (exists y : _, g x y) -> D x). -intro; set (f0 := mkfamily D g H3); assert (H4 := H f0); - cut (covering_open_set X f0). -intro; assert (H6 := H4 H5); elim H6; clear H6; intros D' H6. -unfold covering_finite in H6; decompose [and] H6; - unfold covering, subfamily in H7; simpl in H7; - unfold family_finite, subfamily in H8; simpl in H8; - unfold domain_finite in H8; elim H8; clear H8; intros l H8; - set (alp := MinRlist (AbsList l x)); cut (0 < alp). -intro; assert (H10 := H0 (disc x (mkposreal _ H9))); - cut (neighbourhood (disc x (mkposreal alp H9)) x). -intro; assert (H12 := H10 H11); elim H12; clear H12; intros y H12; - unfold intersection_domain in H12; elim H12; clear H12; - intros; assert (H14 := H7 _ H13); elim H14; clear H14; - intros y0 H14; elim H14; clear H14; intros; unfold g in H14; - elim H14; clear H14; intros; unfold disc in H12; simpl in H12; - cut (alp <= Rabs (y0 - x) / 2). -intro; assert (H18 := Rlt_le_trans _ _ _ H12 H17); - cut (Rabs (y0 - x) < Rabs (y0 - x)). -intro; elim (Rlt_irrefl _ H19). -apply Rle_lt_trans with (Rabs (y0 - y) + Rabs (y - x)). -replace (y0 - x) with (y0 - y + (y - x)); [ apply Rabs_triang | ring ]. -rewrite (double_var (Rabs (y0 - x))); apply Rplus_lt_compat; assumption. -apply (MinRlist_P1 (AbsList l x) (Rabs (y0 - x) / 2)); apply AbsList_P1; - elim (H8 y0); clear H8; intros; apply H8; unfold intersection_domain in |- *; - split; assumption. -assert (H11 := disc_P1 x (mkposreal alp H9)); unfold open_set in H11; - apply H11. -unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; - rewrite Rabs_R0; apply H9. -unfold alp in |- *; apply MinRlist_P2; intros; - assert (H10 := AbsList_P2 _ _ _ H9); elim H10; clear H10; - intros z H10; elim H10; clear H10; intros; rewrite H11; - apply H2; elim (H8 z); clear H8; intros; assert (H13 := H12 H10); - unfold intersection_domain, D in H13; elim H13; clear H13; - intros; assumption. -unfold covering_open_set in |- *; split. -unfold covering in |- *; intros; exists x0; simpl in |- *; unfold g in |- *; - split. -unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; - unfold Rminus in H2; apply (H2 _ H5). -apply H5. -unfold family_open_set in |- *; intro; simpl in |- *; unfold g in |- *; - elim (classic (D x0)); intro. -apply open_set_P6 with (disc x0 (mkposreal _ (H2 _ H5))). -apply disc_P1. -unfold eq_Dom in |- *; split. -unfold included, disc in |- *; simpl in |- *; intros; split. -rewrite <- (Rabs_Ropp (x0 - x1)); rewrite Ropp_minus_distr; apply H6. -apply H5. -unfold included, disc in |- *; simpl in |- *; intros; elim H6; intros; - rewrite <- (Rabs_Ropp (x1 - x0)); rewrite Ropp_minus_distr; - apply H7. -apply open_set_P6 with (fun z:R => False). -apply open_set_P4. -unfold eq_Dom in |- *; split. -unfold included in |- *; intros; elim H6. -unfold included in |- *; intros; elim H6; intros; elim H5; assumption. -intros; elim H3; intros; unfold g in H4; elim H4; clear H4; intros _ H4; - apply H4. -intros; unfold Rdiv in |- *; apply Rmult_lt_0_compat. -apply Rabs_pos_lt; apply Rminus_eq_contra; red in |- *; intro; - rewrite H3 in H2; elim H1; apply H2. -apply Rinv_0_lt_compat; prove_sup0. +Proof. + intros; assert (H0 := closed_set_P1 X); elim H0; clear H0; intros _ H0; + apply H0; clear H0. + unfold eq_Dom in |- *; split. + apply adherence_P1. + unfold included in |- *; unfold adherence in |- *; + unfold point_adherent in |- *; intros; unfold compact in H; + assert (H1 := classic (X x)); elim H1; clear H1; intro. + assumption. + cut (forall y:R, X y -> 0 < Rabs (y - x) / 2). + intro; set (D := X); + set (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y); + cut (forall x:R, (exists y : _, g x y) -> D x). + intro; set (f0 := mkfamily D g H3); assert (H4 := H f0); + cut (covering_open_set X f0). + intro; assert (H6 := H4 H5); elim H6; clear H6; intros D' H6. + unfold covering_finite in H6; decompose [and] H6; + unfold covering, subfamily in H7; simpl in H7; + unfold family_finite, subfamily in H8; simpl in H8; + unfold domain_finite in H8; elim H8; clear H8; intros l H8; + set (alp := MinRlist (AbsList l x)); cut (0 < alp). + intro; assert (H10 := H0 (disc x (mkposreal _ H9))); + cut (neighbourhood (disc x (mkposreal alp H9)) x). + intro; assert (H12 := H10 H11); elim H12; clear H12; intros y H12; + unfold intersection_domain in H12; elim H12; clear H12; + intros; assert (H14 := H7 _ H13); elim H14; clear H14; + intros y0 H14; elim H14; clear H14; intros; unfold g in H14; + elim H14; clear H14; intros; unfold disc in H12; simpl in H12; + cut (alp <= Rabs (y0 - x) / 2). + intro; assert (H18 := Rlt_le_trans _ _ _ H12 H17); + cut (Rabs (y0 - x) < Rabs (y0 - x)). + intro; elim (Rlt_irrefl _ H19). + apply Rle_lt_trans with (Rabs (y0 - y) + Rabs (y - x)). + replace (y0 - x) with (y0 - y + (y - x)); [ apply Rabs_triang | ring ]. + rewrite (double_var (Rabs (y0 - x))); apply Rplus_lt_compat; assumption. + apply (MinRlist_P1 (AbsList l x) (Rabs (y0 - x) / 2)); apply AbsList_P1; + elim (H8 y0); clear H8; intros; apply H8; unfold intersection_domain in |- *; + split; assumption. + assert (H11 := disc_P1 x (mkposreal alp H9)); unfold open_set in H11; + apply H11. + unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; + rewrite Rabs_R0; apply H9. + unfold alp in |- *; apply MinRlist_P2; intros; + assert (H10 := AbsList_P2 _ _ _ H9); elim H10; clear H10; + intros z H10; elim H10; clear H10; intros; rewrite H11; + apply H2; elim (H8 z); clear H8; intros; assert (H13 := H12 H10); + unfold intersection_domain, D in H13; elim H13; clear H13; + intros; assumption. + unfold covering_open_set in |- *; split. + unfold covering in |- *; intros; exists x0; simpl in |- *; unfold g in |- *; + split. + unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + unfold Rminus in H2; apply (H2 _ H5). + apply H5. + unfold family_open_set in |- *; intro; simpl in |- *; unfold g in |- *; + elim (classic (D x0)); intro. + apply open_set_P6 with (disc x0 (mkposreal _ (H2 _ H5))). + apply disc_P1. + unfold eq_Dom in |- *; split. + unfold included, disc in |- *; simpl in |- *; intros; split. + rewrite <- (Rabs_Ropp (x0 - x1)); rewrite Ropp_minus_distr; apply H6. + apply H5. + unfold included, disc in |- *; simpl in |- *; intros; elim H6; intros; + rewrite <- (Rabs_Ropp (x1 - x0)); rewrite Ropp_minus_distr; + apply H7. + apply open_set_P6 with (fun z:R => False). + apply open_set_P4. + unfold eq_Dom in |- *; split. + unfold included in |- *; intros; elim H6. + unfold included in |- *; intros; elim H6; intros; elim H5; assumption. + intros; elim H3; intros; unfold g in H4; elim H4; clear H4; intros _ H4; + apply H4. + intros; unfold Rdiv in |- *; apply Rmult_lt_0_compat. + apply Rabs_pos_lt; apply Rminus_eq_contra; red in |- *; intro; + rewrite H3 in H2; elim H1; apply H2. + apply Rinv_0_lt_compat; prove_sup0. Qed. (**********) Lemma compact_EMP : compact (fun _:R => False). -unfold compact in |- *; intros; exists (fun x:R => False); - unfold covering_finite in |- *; split. -unfold covering in |- *; intros; elim H0. -unfold family_finite in |- *; unfold domain_finite in |- *; exists nil; intro. -split. -simpl in |- *; unfold intersection_domain in |- *; intros; elim H0. -elim H0; clear H0; intros _ H0; elim H0. -simpl in |- *; intro; elim H0. +Proof. + unfold compact in |- *; intros; exists (fun x:R => False); + unfold covering_finite in |- *; split. + unfold covering in |- *; intros; elim H0. + unfold family_finite in |- *; unfold domain_finite in |- *; exists nil; intro. + split. + simpl in |- *; unfold intersection_domain in |- *; intros; elim H0. + elim H0; clear H0; intros _ H0; elim H0. + simpl in |- *; intro; elim H0. Qed. Lemma compact_eqDom : - forall X1 X2:R -> Prop, compact X1 -> X1 =_D X2 -> compact X2. -unfold compact in |- *; intros; unfold eq_Dom in H0; elim H0; clear H0; - unfold included in |- *; intros; assert (H3 : covering_open_set X1 f0). -unfold covering_open_set in |- *; unfold covering_open_set in H1; elim H1; - clear H1; intros; split. -unfold covering in H1; unfold covering in |- *; intros; - apply (H1 _ (H0 _ H4)). -apply H3. -elim (H _ H3); intros D H4; exists D; unfold covering_finite in |- *; - unfold covering_finite in H4; elim H4; intros; split. -unfold covering in H5; unfold covering in |- *; intros; - apply (H5 _ (H2 _ H7)). -apply H6. + forall X1 X2:R -> Prop, compact X1 -> X1 =_D X2 -> compact X2. +Proof. + unfold compact in |- *; intros; unfold eq_Dom in H0; elim H0; clear H0; + unfold included in |- *; intros; assert (H3 : covering_open_set X1 f0). + unfold covering_open_set in |- *; unfold covering_open_set in H1; elim H1; + clear H1; intros; split. + unfold covering in H1; unfold covering in |- *; intros; + apply (H1 _ (H0 _ H4)). + apply H3. + elim (H _ H3); intros D H4; exists D; unfold covering_finite in |- *; + unfold covering_finite in H4; elim H4; intros; split. + unfold covering in H5; unfold covering in |- *; intros; + apply (H5 _ (H2 _ H7)). + apply H6. Qed. -(* Borel-Lebesgue's lemma *) +(** Borel-Lebesgue's lemma *) Lemma compact_P3 : forall a b:R, compact (fun c:R => a <= c <= b). -intros; case (Rle_dec a b); intro. -unfold compact in |- *; intros; - set - (A := - fun x:R => - a <= x <= b /\ - (exists D : R -> Prop, - covering_finite (fun c:R => a <= c <= x) (subfamily f0 D))); - cut (A a). -intro; cut (bound A). -intro; cut (exists a0 : R, A a0). -intro; assert (H3 := completeness A H1 H2); elim H3; clear H3; intros m H3; - unfold is_lub in H3; cut (a <= m <= b). -intro; unfold covering_open_set in H; elim H; clear H; intros; - unfold covering in H; assert (H6 := H m H4); elim H6; - clear H6; intros y0 H6; unfold family_open_set in H5; - assert (H7 := H5 y0); unfold open_set in H7; assert (H8 := H7 m H6); - unfold neighbourhood in H8; elim H8; clear H8; intros eps H8; - cut (exists x : R, A x /\ m - eps < x <= m). -intro; elim H9; clear H9; intros x H9; elim H9; clear H9; intros; - case (Req_dec m b); intro. -rewrite H11 in H10; rewrite H11 in H8; unfold A in H9; elim H9; clear H9; - intros; elim H12; clear H12; intros Dx H12; - set (Db := fun x:R => Dx x \/ x = y0); exists Db; - unfold covering_finite in |- *; split. -unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12; - intros; unfold covering in H12; case (Rle_dec x0 x); - intro. -cut (a <= x0 <= x). -intro; assert (H16 := H12 x0 H15); elim H16; clear H16; intros; exists x1; - simpl in H16; simpl in |- *; unfold Db in |- *; elim H16; - clear H16; intros; split; [ apply H16 | left; apply H17 ]. -split. -elim H14; intros; assumption. -assumption. -exists y0; simpl in |- *; split. -apply H8; unfold disc in |- *; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; - rewrite Rabs_right. -apply Rlt_trans with (b - x). -unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar; - auto with real. -elim H10; intros H15 _; apply Rplus_lt_reg_r with (x - eps); - replace (x - eps + (b - x)) with (b - eps); - [ replace (x - eps + eps) with x; [ apply H15 | ring ] | ring ]. -apply Rge_minus; apply Rle_ge; elim H14; intros _ H15; apply H15. -unfold Db in |- *; right; reflexivity. -unfold family_finite in |- *; unfold domain_finite in |- *; - unfold covering_finite in H12; elim H12; clear H12; - intros; unfold family_finite in H13; unfold domain_finite in H13; - elim H13; clear H13; intros l H13; exists (cons y0 l); - intro; split. -intro; simpl in H14; unfold intersection_domain in H14; elim (H13 x0); - clear H13; intros; case (Req_dec x0 y0); intro. -simpl in |- *; left; apply H16. -simpl in |- *; right; apply H13. -simpl in |- *; unfold intersection_domain in |- *; unfold Db in H14; - decompose [and or] H14. -split; assumption. -elim H16; assumption. -intro; simpl in H14; elim H14; intro; simpl in |- *; - unfold intersection_domain in |- *. -split. -apply (cond_fam f0); rewrite H15; exists m; apply H6. -unfold Db in |- *; right; assumption. -simpl in |- *; unfold intersection_domain in |- *; elim (H13 x0). -intros _ H16; assert (H17 := H16 H15); simpl in H17; - unfold intersection_domain in H17; split. -elim H17; intros; assumption. -unfold Db in |- *; left; elim H17; intros; assumption. -set (m' := Rmin (m + eps / 2) b); cut (A m'). -intro; elim H3; intros; unfold is_upper_bound in H13; - assert (H15 := H13 m' H12); cut (m < m'). -intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H15 H16)). -unfold m' in |- *; unfold Rmin in |- *; case (Rle_dec (m + eps / 2) b); intro. -pattern m at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; - unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. -elim H4; intros. -elim H17; intro. -assumption. -elim H11; assumption. -unfold A in |- *; split. -split. -apply Rle_trans with m. -elim H4; intros; assumption. -unfold m' in |- *; unfold Rmin in |- *; case (Rle_dec (m + eps / 2) b); intro. -pattern m at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; - unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. -elim H4; intros. -elim H13; intro. -assumption. -elim H11; assumption. -unfold m' in |- *; apply Rmin_r. -unfold A in H9; elim H9; clear H9; intros; elim H12; clear H12; intros Dx H12; - set (Db := fun x:R => Dx x \/ x = y0); exists Db; - unfold covering_finite in |- *; split. -unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12; - intros; unfold covering in H12; case (Rle_dec x0 x); - intro. -cut (a <= x0 <= x). -intro; assert (H16 := H12 x0 H15); elim H16; clear H16; intros; exists x1; - simpl in H16; simpl in |- *; unfold Db in |- *. -elim H16; clear H16; intros; split; [ apply H16 | left; apply H17 ]. -elim H14; intros; split; assumption. -exists y0; simpl in |- *; split. -apply H8; unfold disc in |- *; unfold Rabs in |- *; case (Rcase_abs (x0 - m)); - intro. -rewrite Ropp_minus_distr; apply Rlt_trans with (m - x). -unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar; - auto with real. -apply Rplus_lt_reg_r with (x - eps); - replace (x - eps + (m - x)) with (m - eps). -replace (x - eps + eps) with x. -elim H10; intros; assumption. -ring. -ring. -apply Rle_lt_trans with (m' - m). -unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (- m)); - apply Rplus_le_compat_l; elim H14; intros; assumption. -apply Rplus_lt_reg_r with m; replace (m + (m' - m)) with m'. -apply Rle_lt_trans with (m + eps / 2). -unfold m' in |- *; apply Rmin_l. -apply Rplus_lt_compat_l; apply Rmult_lt_reg_l with 2. -prove_sup0. -unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; - rewrite <- Rinv_r_sym. -rewrite Rmult_1_l; pattern (pos eps) at 1 in |- *; rewrite <- Rplus_0_r; - rewrite double; apply Rplus_lt_compat_l; apply (cond_pos eps). -discrR. -ring. -unfold Db in |- *; right; reflexivity. -unfold family_finite in |- *; unfold domain_finite in |- *; - unfold covering_finite in H12; elim H12; clear H12; - intros; unfold family_finite in H13; unfold domain_finite in H13; - elim H13; clear H13; intros l H13; exists (cons y0 l); - intro; split. -intro; simpl in H14; unfold intersection_domain in H14; elim (H13 x0); - clear H13; intros; case (Req_dec x0 y0); intro. -simpl in |- *; left; apply H16. -simpl in |- *; right; apply H13; simpl in |- *; - unfold intersection_domain in |- *; unfold Db in H14; - decompose [and or] H14. -split; assumption. -elim H16; assumption. -intro; simpl in H14; elim H14; intro; simpl in |- *; - unfold intersection_domain in |- *. -split. -apply (cond_fam f0); rewrite H15; exists m; apply H6. -unfold Db in |- *; right; assumption. -elim (H13 x0); intros _ H16. -assert (H17 := H16 H15). -simpl in H17. -unfold intersection_domain in H17. -split. -elim H17; intros; assumption. -unfold Db in |- *; left; elim H17; intros; assumption. -elim (classic (exists x : R, A x /\ m - eps < x <= m)); intro. -assumption. -elim H3; intros; cut (is_upper_bound A (m - eps)). -intro; assert (H13 := H11 _ H12); cut (m - eps < m). -intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H14)). -pattern m at 2 in |- *; rewrite <- Rplus_0_r; unfold Rminus in |- *; - apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_involutive; - rewrite Ropp_0; apply (cond_pos eps). -set (P := fun n:R => A n /\ m - eps < n <= m); - assert (H12 := not_ex_all_not _ P H9); unfold P in H12; - unfold is_upper_bound in |- *; intros; - assert (H14 := not_and_or _ _ (H12 x)); elim H14; - intro. -elim H15; apply H13. -elim (not_and_or _ _ H15); intro. -case (Rle_dec x (m - eps)); intro. -assumption. -elim H16; auto with real. -unfold is_upper_bound in H10; assert (H17 := H10 x H13); elim H16; apply H17. -elim H3; clear H3; intros. -unfold is_upper_bound in H3. -split. -apply (H3 _ H0). -apply (H4 b); unfold is_upper_bound in |- *; intros; unfold A in H5; elim H5; - clear H5; intros H5 _; elim H5; clear H5; intros _ H5; - apply H5. -exists a; apply H0. -unfold bound in |- *; exists b; unfold is_upper_bound in |- *; intros; - unfold A in H1; elim H1; clear H1; intros H1 _; elim H1; - clear H1; intros _ H1; apply H1. -unfold A in |- *; split. -split; [ right; reflexivity | apply r ]. -unfold covering_open_set in H; elim H; clear H; intros; unfold covering in H; - cut (a <= a <= b). -intro; elim (H _ H1); intros y0 H2; set (D' := fun x:R => x = y0); exists D'; - unfold covering_finite in |- *; split. -unfold covering in |- *; simpl in |- *; intros; cut (x = a). -intro; exists y0; split. -rewrite H4; apply H2. -unfold D' in |- *; reflexivity. -elim H3; intros; apply Rle_antisym; assumption. -unfold family_finite in |- *; unfold domain_finite in |- *; - exists (cons y0 nil); intro; split. -simpl in |- *; unfold intersection_domain in |- *; intro; elim H3; clear H3; - intros; unfold D' in H4; left; apply H4. -simpl in |- *; unfold intersection_domain in |- *; intro; elim H3; intro. -split; [ rewrite H4; apply (cond_fam f0); exists a; apply H2 | apply H4 ]. -elim H4. -split; [ right; reflexivity | apply r ]. -apply compact_eqDom with (fun c:R => False). -apply compact_EMP. -unfold eq_Dom in |- *; split. -unfold included in |- *; intros; elim H. -unfold included in |- *; intros; elim H; clear H; intros; - assert (H1 := Rle_trans _ _ _ H H0); elim n; apply H1. +Proof. + intros; case (Rle_dec a b); intro. + unfold compact in |- *; intros; + set + (A := + fun x:R => + a <= x <= b /\ + (exists D : R -> Prop, + covering_finite (fun c:R => a <= c <= x) (subfamily f0 D))); + cut (A a). + intro; cut (bound A). + intro; cut (exists a0 : R, A a0). + intro; assert (H3 := completeness A H1 H2); elim H3; clear H3; intros m H3; + unfold is_lub in H3; cut (a <= m <= b). + intro; unfold covering_open_set in H; elim H; clear H; intros; + unfold covering in H; assert (H6 := H m H4); elim H6; + clear H6; intros y0 H6; unfold family_open_set in H5; + assert (H7 := H5 y0); unfold open_set in H7; assert (H8 := H7 m H6); + unfold neighbourhood in H8; elim H8; clear H8; intros eps H8; + cut (exists x : R, A x /\ m - eps < x <= m). + intro; elim H9; clear H9; intros x H9; elim H9; clear H9; intros; + case (Req_dec m b); intro. + rewrite H11 in H10; rewrite H11 in H8; unfold A in H9; elim H9; clear H9; + intros; elim H12; clear H12; intros Dx H12; + set (Db := fun x:R => Dx x \/ x = y0); exists Db; + unfold covering_finite in |- *; split. + unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12; + intros; unfold covering in H12; case (Rle_dec x0 x); + intro. + cut (a <= x0 <= x). + intro; assert (H16 := H12 x0 H15); elim H16; clear H16; intros; exists x1; + simpl in H16; simpl in |- *; unfold Db in |- *; elim H16; + clear H16; intros; split; [ apply H16 | left; apply H17 ]. + split. + elim H14; intros; assumption. + assumption. + exists y0; simpl in |- *; split. + apply H8; unfold disc in |- *; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; + rewrite Rabs_right. + apply Rlt_trans with (b - x). + unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar; + auto with real. + elim H10; intros H15 _; apply Rplus_lt_reg_r with (x - eps); + replace (x - eps + (b - x)) with (b - eps); + [ replace (x - eps + eps) with x; [ apply H15 | ring ] | ring ]. + apply Rge_minus; apply Rle_ge; elim H14; intros _ H15; apply H15. + unfold Db in |- *; right; reflexivity. + unfold family_finite in |- *; unfold domain_finite in |- *; + unfold covering_finite in H12; elim H12; clear H12; + intros; unfold family_finite in H13; unfold domain_finite in H13; + elim H13; clear H13; intros l H13; exists (cons y0 l); + intro; split. + intro; simpl in H14; unfold intersection_domain in H14; elim (H13 x0); + clear H13; intros; case (Req_dec x0 y0); intro. + simpl in |- *; left; apply H16. + simpl in |- *; right; apply H13. + simpl in |- *; unfold intersection_domain in |- *; unfold Db in H14; + decompose [and or] H14. + split; assumption. + elim H16; assumption. + intro; simpl in H14; elim H14; intro; simpl in |- *; + unfold intersection_domain in |- *. + split. + apply (cond_fam f0); rewrite H15; exists m; apply H6. + unfold Db in |- *; right; assumption. + simpl in |- *; unfold intersection_domain in |- *; elim (H13 x0). + intros _ H16; assert (H17 := H16 H15); simpl in H17; + unfold intersection_domain in H17; split. + elim H17; intros; assumption. + unfold Db in |- *; left; elim H17; intros; assumption. + set (m' := Rmin (m + eps / 2) b); cut (A m'). + intro; elim H3; intros; unfold is_upper_bound in H13; + assert (H15 := H13 m' H12); cut (m < m'). + intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H15 H16)). + unfold m' in |- *; unfold Rmin in |- *; case (Rle_dec (m + eps / 2) b); intro. + pattern m at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; + unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. + elim H4; intros. + elim H17; intro. + assumption. + elim H11; assumption. + unfold A in |- *; split. + split. + apply Rle_trans with m. + elim H4; intros; assumption. + unfold m' in |- *; unfold Rmin in |- *; case (Rle_dec (m + eps / 2) b); intro. + pattern m at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; + unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. + elim H4; intros. + elim H13; intro. + assumption. + elim H11; assumption. + unfold m' in |- *; apply Rmin_r. + unfold A in H9; elim H9; clear H9; intros; elim H12; clear H12; intros Dx H12; + set (Db := fun x:R => Dx x \/ x = y0); exists Db; + unfold covering_finite in |- *; split. + unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12; + intros; unfold covering in H12; case (Rle_dec x0 x); + intro. + cut (a <= x0 <= x). + intro; assert (H16 := H12 x0 H15); elim H16; clear H16; intros; exists x1; + simpl in H16; simpl in |- *; unfold Db in |- *. + elim H16; clear H16; intros; split; [ apply H16 | left; apply H17 ]. + elim H14; intros; split; assumption. + exists y0; simpl in |- *; split. + apply H8; unfold disc in |- *; unfold Rabs in |- *; case (Rcase_abs (x0 - m)); + intro. + rewrite Ropp_minus_distr; apply Rlt_trans with (m - x). + unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar; + auto with real. + apply Rplus_lt_reg_r with (x - eps); + replace (x - eps + (m - x)) with (m - eps). + replace (x - eps + eps) with x. + elim H10; intros; assumption. + ring. + ring. + apply Rle_lt_trans with (m' - m). + unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (- m)); + apply Rplus_le_compat_l; elim H14; intros; assumption. + apply Rplus_lt_reg_r with m; replace (m + (m' - m)) with m'. + apply Rle_lt_trans with (m + eps / 2). + unfold m' in |- *; apply Rmin_l. + apply Rplus_lt_compat_l; apply Rmult_lt_reg_l with 2. + prove_sup0. + unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + rewrite <- Rinv_r_sym. + rewrite Rmult_1_l; pattern (pos eps) at 1 in |- *; rewrite <- Rplus_0_r; + rewrite double; apply Rplus_lt_compat_l; apply (cond_pos eps). + discrR. + ring. + unfold Db in |- *; right; reflexivity. + unfold family_finite in |- *; unfold domain_finite in |- *; + unfold covering_finite in H12; elim H12; clear H12; + intros; unfold family_finite in H13; unfold domain_finite in H13; + elim H13; clear H13; intros l H13; exists (cons y0 l); + intro; split. + intro; simpl in H14; unfold intersection_domain in H14; elim (H13 x0); + clear H13; intros; case (Req_dec x0 y0); intro. + simpl in |- *; left; apply H16. + simpl in |- *; right; apply H13; simpl in |- *; + unfold intersection_domain in |- *; unfold Db in H14; + decompose [and or] H14. + split; assumption. + elim H16; assumption. + intro; simpl in H14; elim H14; intro; simpl in |- *; + unfold intersection_domain in |- *. + split. + apply (cond_fam f0); rewrite H15; exists m; apply H6. + unfold Db in |- *; right; assumption. + elim (H13 x0); intros _ H16. + assert (H17 := H16 H15). + simpl in H17. + unfold intersection_domain in H17. + split. + elim H17; intros; assumption. + unfold Db in |- *; left; elim H17; intros; assumption. + elim (classic (exists x : R, A x /\ m - eps < x <= m)); intro. + assumption. + elim H3; intros; cut (is_upper_bound A (m - eps)). + intro; assert (H13 := H11 _ H12); cut (m - eps < m). + intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H14)). + pattern m at 2 in |- *; rewrite <- Rplus_0_r; unfold Rminus in |- *; + apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_involutive; + rewrite Ropp_0; apply (cond_pos eps). + set (P := fun n:R => A n /\ m - eps < n <= m); + assert (H12 := not_ex_all_not _ P H9); unfold P in H12; + unfold is_upper_bound in |- *; intros; + assert (H14 := not_and_or _ _ (H12 x)); elim H14; + intro. + elim H15; apply H13. + elim (not_and_or _ _ H15); intro. + case (Rle_dec x (m - eps)); intro. + assumption. + elim H16; auto with real. + unfold is_upper_bound in H10; assert (H17 := H10 x H13); elim H16; apply H17. + elim H3; clear H3; intros. + unfold is_upper_bound in H3. + split. + apply (H3 _ H0). + apply (H4 b); unfold is_upper_bound in |- *; intros; unfold A in H5; elim H5; + clear H5; intros H5 _; elim H5; clear H5; intros _ H5; + apply H5. + exists a; apply H0. + unfold bound in |- *; exists b; unfold is_upper_bound in |- *; intros; + unfold A in H1; elim H1; clear H1; intros H1 _; elim H1; + clear H1; intros _ H1; apply H1. + unfold A in |- *; split. + split; [ right; reflexivity | apply r ]. + unfold covering_open_set in H; elim H; clear H; intros; unfold covering in H; + cut (a <= a <= b). + intro; elim (H _ H1); intros y0 H2; set (D' := fun x:R => x = y0); exists D'; + unfold covering_finite in |- *; split. + unfold covering in |- *; simpl in |- *; intros; cut (x = a). + intro; exists y0; split. + rewrite H4; apply H2. + unfold D' in |- *; reflexivity. + elim H3; intros; apply Rle_antisym; assumption. + unfold family_finite in |- *; unfold domain_finite in |- *; + exists (cons y0 nil); intro; split. + simpl in |- *; unfold intersection_domain in |- *; intro; elim H3; clear H3; + intros; unfold D' in H4; left; apply H4. + simpl in |- *; unfold intersection_domain in |- *; intro; elim H3; intro. + split; [ rewrite H4; apply (cond_fam f0); exists a; apply H2 | apply H4 ]. + elim H4. + split; [ right; reflexivity | apply r ]. + apply compact_eqDom with (fun c:R => False). + apply compact_EMP. + unfold eq_Dom in |- *; split. + unfold included in |- *; intros; elim H. + unfold included in |- *; intros; elim H; clear H; intros; + assert (H1 := Rle_trans _ _ _ H H0); elim n; apply H1. Qed. Lemma compact_P4 : - forall X F:R -> Prop, compact X -> closed_set F -> included F X -> compact F. -unfold compact in |- *; intros; elim (classic (exists z : R, F z)); - intro Hyp_F_NE. -set (D := ind f0); set (g := f f0); unfold closed_set in H0. -set (g' := fun x y:R => f0 x y \/ complementary F y /\ D x). -set (D' := D). -cut (forall x:R, (exists y : R, g' x y) -> D' x). -intro; set (f' := mkfamily D' g' H3); cut (covering_open_set X f'). -intro; elim (H _ H4); intros DX H5; exists DX. -unfold covering_finite in |- *; unfold covering_finite in H5; elim H5; - clear H5; intros. -split. -unfold covering in |- *; unfold covering in H5; intros. -elim (H5 _ (H1 _ H7)); intros y0 H8; exists y0; simpl in H8; simpl in |- *; - elim H8; clear H8; intros. -split. -unfold g' in H8; elim H8; intro. -apply H10. -elim H10; intros H11 _; unfold complementary in H11; elim H11; apply H7. -apply H9. -unfold family_finite in |- *; unfold domain_finite in |- *; - unfold family_finite in H6; unfold domain_finite in H6; - elim H6; clear H6; intros l H6; exists l; intro; assert (H7 := H6 x); - elim H7; clear H7; intros. -split. -intro; apply H7; simpl in |- *; unfold intersection_domain in |- *; - simpl in H9; unfold intersection_domain in H9; unfold D' in |- *; - apply H9. -intro; assert (H10 := H8 H9); simpl in H10; unfold intersection_domain in H10; - simpl in |- *; unfold intersection_domain in |- *; - unfold D' in H10; apply H10. -unfold covering_open_set in |- *; unfold covering_open_set in H2; elim H2; - clear H2; intros. -split. -unfold covering in |- *; unfold covering in H2; intros. -elim (classic (F x)); intro. -elim (H2 _ H6); intros y0 H7; exists y0; simpl in |- *; unfold g' in |- *; - left; assumption. -cut (exists z : R, D z). -intro; elim H7; clear H7; intros x0 H7; exists x0; simpl in |- *; - unfold g' in |- *; right. -split. -unfold complementary in |- *; apply H6. -apply H7. -elim Hyp_F_NE; intros z0 H7. -assert (H8 := H2 _ H7). -elim H8; clear H8; intros t H8; exists t; apply (cond_fam f0); exists z0; - apply H8. -unfold family_open_set in |- *; intro; simpl in |- *; unfold g' in |- *; - elim (classic (D x)); intro. -apply open_set_P6 with (union_domain (f0 x) (complementary F)). -apply open_set_P2. -unfold family_open_set in H4; apply H4. -apply H0. -unfold eq_Dom in |- *; split. -unfold included, union_domain, complementary in |- *; intros. -elim H6; intro; [ left; apply H7 | right; split; assumption ]. -unfold included, union_domain, complementary in |- *; intros. -elim H6; intro; [ left; apply H7 | right; elim H7; intros; apply H8 ]. -apply open_set_P6 with (f0 x). -unfold family_open_set in H4; apply H4. -unfold eq_Dom in |- *; split. -unfold included, complementary in |- *; intros; left; apply H6. -unfold included, complementary in |- *; intros. -elim H6; intro. -apply H7. -elim H7; intros _ H8; elim H5; apply H8. -intros; elim H3; intros y0 H4; unfold g' in H4; elim H4; intro. -apply (cond_fam f0); exists y0; apply H5. -elim H5; clear H5; intros _ H5; apply H5. + forall X F:R -> Prop, compact X -> closed_set F -> included F X -> compact F. +Proof. + unfold compact in |- *; intros; elim (classic (exists z : R, F z)); + intro Hyp_F_NE. + set (D := ind f0); set (g := f f0); unfold closed_set in H0. + set (g' := fun x y:R => f0 x y \/ complementary F y /\ D x). + set (D' := D). + cut (forall x:R, (exists y : R, g' x y) -> D' x). + intro; set (f' := mkfamily D' g' H3); cut (covering_open_set X f'). + intro; elim (H _ H4); intros DX H5; exists DX. + unfold covering_finite in |- *; unfold covering_finite in H5; elim H5; + clear H5; intros. + split. + unfold covering in |- *; unfold covering in H5; intros. + elim (H5 _ (H1 _ H7)); intros y0 H8; exists y0; simpl in H8; simpl in |- *; + elim H8; clear H8; intros. + split. + unfold g' in H8; elim H8; intro. + apply H10. + elim H10; intros H11 _; unfold complementary in H11; elim H11; apply H7. + apply H9. + unfold family_finite in |- *; unfold domain_finite in |- *; + unfold family_finite in H6; unfold domain_finite in H6; + elim H6; clear H6; intros l H6; exists l; intro; assert (H7 := H6 x); + elim H7; clear H7; intros. + split. + intro; apply H7; simpl in |- *; unfold intersection_domain in |- *; + simpl in H9; unfold intersection_domain in H9; unfold D' in |- *; + apply H9. + intro; assert (H10 := H8 H9); simpl in H10; unfold intersection_domain in H10; + simpl in |- *; unfold intersection_domain in |- *; + unfold D' in H10; apply H10. + unfold covering_open_set in |- *; unfold covering_open_set in H2; elim H2; + clear H2; intros. + split. + unfold covering in |- *; unfold covering in H2; intros. + elim (classic (F x)); intro. + elim (H2 _ H6); intros y0 H7; exists y0; simpl in |- *; unfold g' in |- *; + left; assumption. + cut (exists z : R, D z). + intro; elim H7; clear H7; intros x0 H7; exists x0; simpl in |- *; + unfold g' in |- *; right. + split. + unfold complementary in |- *; apply H6. + apply H7. + elim Hyp_F_NE; intros z0 H7. + assert (H8 := H2 _ H7). + elim H8; clear H8; intros t H8; exists t; apply (cond_fam f0); exists z0; + apply H8. + unfold family_open_set in |- *; intro; simpl in |- *; unfold g' in |- *; + elim (classic (D x)); intro. + apply open_set_P6 with (union_domain (f0 x) (complementary F)). + apply open_set_P2. + unfold family_open_set in H4; apply H4. + apply H0. + unfold eq_Dom in |- *; split. + unfold included, union_domain, complementary in |- *; intros. + elim H6; intro; [ left; apply H7 | right; split; assumption ]. + unfold included, union_domain, complementary in |- *; intros. + elim H6; intro; [ left; apply H7 | right; elim H7; intros; apply H8 ]. + apply open_set_P6 with (f0 x). + unfold family_open_set in H4; apply H4. + unfold eq_Dom in |- *; split. + unfold included, complementary in |- *; intros; left; apply H6. + unfold included, complementary in |- *; intros. + elim H6; intro. + apply H7. + elim H7; intros _ H8; elim H5; apply H8. + intros; elim H3; intros y0 H4; unfold g' in H4; elim H4; intro. + apply (cond_fam f0); exists y0; apply H5. + elim H5; clear H5; intros _ H5; apply H5. (* Cas ou F est l'ensemble vide *) -cut (compact F). -intro; apply (H3 f0 H2). -apply compact_eqDom with (fun _:R => False). -apply compact_EMP. -unfold eq_Dom in |- *; split. -unfold included in |- *; intros; elim H3. -assert (H3 := not_ex_all_not _ _ Hyp_F_NE); unfold included in |- *; intros; - elim (H3 x); apply H4. + cut (compact F). + intro; apply (H3 f0 H2). + apply compact_eqDom with (fun _:R => False). + apply compact_EMP. + unfold eq_Dom in |- *; split. + unfold included in |- *; intros; elim H3. + assert (H3 := not_ex_all_not _ _ Hyp_F_NE); unfold included in |- *; intros; + elim (H3 x); apply H4. Qed. (**********) Lemma compact_P5 : forall X:R -> Prop, closed_set X -> bounded X -> compact X. -intros; unfold bounded in H0. -elim H0; clear H0; intros m H0. -elim H0; clear H0; intros M H0. -assert (H1 := compact_P3 m M). -apply (compact_P4 (fun c:R => m <= c <= M) X H1 H H0). +Proof. + intros; unfold bounded in H0. + elim H0; clear H0; intros m H0. + elim H0; clear H0; intros M H0. + assert (H1 := compact_P3 m M). + apply (compact_P4 (fun c:R => m <= c <= M) X H1 H H0). Qed. (**********) Lemma compact_carac : - forall X:R -> Prop, compact X <-> closed_set X /\ bounded X. -intro; split. -intro; split; [ apply (compact_P2 _ H) | apply (compact_P1 _ H) ]. -intro; elim H; clear H; intros; apply (compact_P5 _ H H0). + forall X:R -> Prop, compact X <-> closed_set X /\ bounded X. +Proof. + intro; split. + intro; split; [ apply (compact_P2 _ H) | apply (compact_P1 _ H) ]. + intro; elim H; clear H; intros; apply (compact_P5 _ H H0). Qed. Definition image_dir (f:R -> R) (D:R -> Prop) (x:R) : Prop := - exists y : R, x = f y /\ D y. + exists y : R, x = f y /\ D y. (**********) Lemma continuity_compact : - forall (f:R -> R) (X:R -> Prop), - (forall x:R, continuity_pt f x) -> compact X -> compact (image_dir f X). -unfold compact in |- *; intros; unfold covering_open_set in H1. -elim H1; clear H1; intros. -set (D := ind f1). -set (g := fun x y:R => image_rec f0 (f1 x) y). -cut (forall x:R, (exists y : R, g x y) -> D x). -intro; set (f' := mkfamily D g H3). -cut (covering_open_set X f'). -intro; elim (H0 f' H4); intros D' H5; exists D'. -unfold covering_finite in H5; elim H5; clear H5; intros; - unfold covering_finite in |- *; split. -unfold covering, image_dir in |- *; simpl in |- *; unfold covering in H5; - intros; elim H7; intros y H8; elim H8; intros; assert (H11 := H5 _ H10); - simpl in H11; elim H11; intros z H12; exists z; unfold g in H12; - unfold image_rec in H12; rewrite H9; apply H12. -unfold family_finite in H6; unfold domain_finite in H6; - unfold family_finite in |- *; unfold domain_finite in |- *; - elim H6; intros l H7; exists l; intro; elim (H7 x); - intros; split; intro. -apply H8; simpl in H10; simpl in |- *; apply H10. -apply (H9 H10). -unfold covering_open_set in |- *; split. -unfold covering in |- *; intros; simpl in |- *; unfold covering in H1; - unfold image_dir in H1; unfold g in |- *; unfold image_rec in |- *; - apply H1. -exists x; split; [ reflexivity | apply H4 ]. -unfold family_open_set in |- *; unfold family_open_set in H2; intro; - simpl in |- *; unfold g in |- *; - cut ((fun y:R => image_rec f0 (f1 x) y) = image_rec f0 (f1 x)). -intro; rewrite H4. -apply (continuity_P2 f0 (f1 x) H (H2 x)). -reflexivity. -intros; apply (cond_fam f1); unfold g in H3; unfold image_rec in H3; elim H3; - intros; exists (f0 x0); apply H4. + forall (f:R -> R) (X:R -> Prop), + (forall x:R, continuity_pt f x) -> compact X -> compact (image_dir f X). +Proof. + unfold compact in |- *; intros; unfold covering_open_set in H1. + elim H1; clear H1; intros. + set (D := ind f1). + set (g := fun x y:R => image_rec f0 (f1 x) y). + cut (forall x:R, (exists y : R, g x y) -> D x). + intro; set (f' := mkfamily D g H3). + cut (covering_open_set X f'). + intro; elim (H0 f' H4); intros D' H5; exists D'. + unfold covering_finite in H5; elim H5; clear H5; intros; + unfold covering_finite in |- *; split. + unfold covering, image_dir in |- *; simpl in |- *; unfold covering in H5; + intros; elim H7; intros y H8; elim H8; intros; assert (H11 := H5 _ H10); + simpl in H11; elim H11; intros z H12; exists z; unfold g in H12; + unfold image_rec in H12; rewrite H9; apply H12. + unfold family_finite in H6; unfold domain_finite in H6; + unfold family_finite in |- *; unfold domain_finite in |- *; + elim H6; intros l H7; exists l; intro; elim (H7 x); + intros; split; intro. + apply H8; simpl in H10; simpl in |- *; apply H10. + apply (H9 H10). + unfold covering_open_set in |- *; split. + unfold covering in |- *; intros; simpl in |- *; unfold covering in H1; + unfold image_dir in H1; unfold g in |- *; unfold image_rec in |- *; + apply H1. + exists x; split; [ reflexivity | apply H4 ]. + unfold family_open_set in |- *; unfold family_open_set in H2; intro; + simpl in |- *; unfold g in |- *; + cut ((fun y:R => image_rec f0 (f1 x) y) = image_rec f0 (f1 x)). + intro; rewrite H4. + apply (continuity_P2 f0 (f1 x) H (H2 x)). + reflexivity. + intros; apply (cond_fam f1); unfold g in H3; unfold image_rec in H3; elim H3; + intros; exists (f0 x0); apply H4. Qed. Lemma Rlt_Rminus : forall a b:R, a < b -> 0 < b - a. -intros; apply Rplus_lt_reg_r with a; rewrite Rplus_0_r; - replace (a + (b - a)) with b; [ assumption | ring ]. +Proof. + intros; apply Rplus_lt_reg_r with a; rewrite Rplus_0_r; + replace (a + (b - a)) with b; [ assumption | ring ]. Qed. Lemma prolongement_C0 : - forall (f:R -> R) (a b:R), - a <= b -> - (forall c:R, a <= c <= b -> continuity_pt f c) -> + 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). -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_Rminus; assumption. -exists h; split. -unfold continuity in |- *; intro; case (Rtotal_order x a); intro. -unfold continuity_pt in |- *; unfold continue_in in |- *; - unfold limit1_in in |- *; unfold limit_in in |- *; - simpl in |- *; unfold R_dist in |- *; intros; exists (a - x); - split. -change (0 < a - x) in |- *; apply Rlt_Rminus; assumption. -intros; elim H5; clear H5; intros _ H5; unfold h in |- *. -case (Rle_dec x a); intro. -case (Rle_dec x0 a); intro. -unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. -elim n; left; apply Rplus_lt_reg_r with (- x); - do 2 rewrite (Rplus_comm (- x)); apply Rle_lt_trans with (Rabs (x0 - x)). -apply RRle_abs. -assumption. -elim n; 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 R_dist in H6; unfold continuity_pt in |- *; - unfold continue_in in |- *; unfold limit1_in in |- *; - unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; - intros; elim (H6 _ H7); intros; exists (Rmin x0 (b - a)); - split. -unfold Rmin in |- *; case (Rle_dec x0 (b - a)); intro. -elim H8; intros; assumption. -change (0 < b - a) in |- *; apply Rlt_Rminus; assumption. -intros; elim H9; clear H9; intros _ H9; cut (x1 < b). -intro; unfold h in |- *; case (Rle_dec x a); intro. -case (Rle_dec x1 a); intro. -unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. -case (Rle_dec x1 b); intro. -elim H8; intros; apply H12; split. -unfold D_x, no_cond in |- *; split. -trivial. -red in |- *; intro; elim n; right; symmetry in |- *; assumption. -apply Rlt_le_trans with (Rmin x0 (b - a)). -rewrite H4 in H9; apply H9. -apply Rmin_l. -elim n0; left; assumption. -elim n; right; assumption. -apply Rplus_lt_reg_r 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 R_dist in H7; unfold continuity_pt in |- *; - unfold continue_in in |- *; unfold limit1_in in |- *; - unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; - intros; elim (H7 _ H8); intros; elim H9; clear H9; - intros. -assert (H11 : 0 < x - a). -apply Rlt_Rminus; assumption. -assert (H12 : 0 < b - x). -apply Rlt_Rminus; assumption. -exists (Rmin x0 (Rmin (x - a) (b - x))); split. -unfold Rmin in |- *; case (Rle_dec (x - a) (b - x)); intro. -case (Rle_dec x0 (x - a)); intro. -assumption. -assumption. -case (Rle_dec x0 (b - x)); intro. -assumption. -assumption. -intros; elim H13; clear H13; intros; cut (a < x1 < b). -intro; elim H15; clear H15; intros; unfold h in |- *; case (Rle_dec x a); - intro. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). -case (Rle_dec x b); intro. -case (Rle_dec x1 a); intro. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H15)). -case (Rle_dec x1 b); intro. -apply H10; split. -assumption. -apply Rlt_le_trans with (Rmin x0 (Rmin (x - a) (b - x))). -assumption. -apply Rmin_l. -elim n1; left; assumption. -elim n0; left; assumption. -split. -apply Ropp_lt_cancel; apply Rplus_lt_reg_r 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_r 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 R_dist in H8; unfold continuity_pt in |- *; - unfold continue_in in |- *; unfold limit1_in in |- *; - unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; - intros; elim (H8 _ H9); intros; exists (Rmin x0 (b - a)); - split. -unfold Rmin in |- *; case (Rle_dec x0 (b - a)); intro. -elim H10; intros; assumption. -change (0 < b - a) in |- *; apply Rlt_Rminus; assumption. -intros; elim H11; clear H11; intros _ H11; cut (a < x1). -intro; unfold h in |- *; case (Rle_dec x a); intro. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). -case (Rle_dec x1 a); intro. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H12)). -case (Rle_dec x b); intro. -case (Rle_dec x1 b); intro. -rewrite H6; elim H10; intros; elim r0; intro. -apply H14; split. -unfold D_x, no_cond in |- *; split. -trivial. -red in |- *; 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 in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; - assumption. -rewrite H6; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; - assumption. -elim n1; right; assumption. -rewrite H6 in H11; apply Ropp_lt_cancel; apply Rplus_lt_reg_r 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 in |- *; unfold continue_in in |- *; - unfold limit1_in in |- *; unfold limit_in in |- *; - simpl in |- *; unfold R_dist in |- *; intros; exists (x - b); - split. -change (0 < x - b) in |- *; apply Rlt_Rminus; assumption. -intros; elim H8; clear H8; intros. -assert (H10 : b < x0). -apply Ropp_lt_cancel; apply Rplus_lt_reg_r with x; - apply Rle_lt_trans with (Rabs (x0 - x)). -rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs. -assumption. -unfold h in |- *; case (Rle_dec x a); intro. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). -case (Rle_dec x b); intro. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H6)). -case (Rle_dec x0 a); intro. -elim (Rlt_irrefl _ (Rlt_trans _ _ _ H1 (Rlt_le_trans _ _ _ H10 r))). -case (Rle_dec x0 b); intro. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H10)). -unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. -intros; elim H3; intros; unfold h in |- *; case (Rle_dec c a); intro. -elim r; intro. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 H6)). -rewrite H6; reflexivity. -case (Rle_dec c b); intro. -reflexivity. -elim n0; 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. + continuity g /\ (forall c:R, a <= c <= b -> g c = f c). +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_Rminus; assumption. + exists h; split. + unfold continuity in |- *; intro; case (Rtotal_order x a); intro. + unfold continuity_pt in |- *; unfold continue_in in |- *; + unfold limit1_in in |- *; unfold limit_in in |- *; + simpl in |- *; unfold R_dist in |- *; intros; exists (a - x); + split. + change (0 < a - x) in |- *; apply Rlt_Rminus; assumption. + intros; elim H5; clear H5; intros _ H5; unfold h in |- *. + case (Rle_dec x a); intro. + case (Rle_dec x0 a); intro. + unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + elim n; left; apply Rplus_lt_reg_r with (- x); + do 2 rewrite (Rplus_comm (- x)); apply Rle_lt_trans with (Rabs (x0 - x)). + apply RRle_abs. + assumption. + elim n; 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 R_dist in H6; unfold continuity_pt in |- *; + unfold continue_in in |- *; unfold limit1_in in |- *; + unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; + intros; elim (H6 _ H7); intros; exists (Rmin x0 (b - a)); + split. + unfold Rmin in |- *; case (Rle_dec x0 (b - a)); intro. + elim H8; intros; assumption. + change (0 < b - a) in |- *; apply Rlt_Rminus; assumption. + intros; elim H9; clear H9; intros _ H9; cut (x1 < b). + intro; unfold h in |- *; case (Rle_dec x a); intro. + case (Rle_dec x1 a); intro. + unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + case (Rle_dec x1 b); intro. + elim H8; intros; apply H12; split. + unfold D_x, no_cond in |- *; split. + trivial. + red in |- *; intro; elim n; right; symmetry in |- *; assumption. + apply Rlt_le_trans with (Rmin x0 (b - a)). + rewrite H4 in H9; apply H9. + apply Rmin_l. + elim n0; left; assumption. + elim n; right; assumption. + apply Rplus_lt_reg_r 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 R_dist in H7; unfold continuity_pt in |- *; + unfold continue_in in |- *; unfold limit1_in in |- *; + unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; + intros; elim (H7 _ H8); intros; elim H9; clear H9; + intros. + assert (H11 : 0 < x - a). + apply Rlt_Rminus; assumption. + assert (H12 : 0 < b - x). + apply Rlt_Rminus; assumption. + exists (Rmin x0 (Rmin (x - a) (b - x))); split. + unfold Rmin in |- *; case (Rle_dec (x - a) (b - x)); intro. + case (Rle_dec x0 (x - a)); intro. + assumption. + assumption. + case (Rle_dec x0 (b - x)); intro. + assumption. + assumption. + intros; elim H13; clear H13; intros; cut (a < x1 < b). + intro; elim H15; clear H15; intros; unfold h in |- *; case (Rle_dec x a); + intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). + case (Rle_dec x b); intro. + case (Rle_dec x1 a); intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H15)). + case (Rle_dec x1 b); intro. + apply H10; split. + assumption. + apply Rlt_le_trans with (Rmin x0 (Rmin (x - a) (b - x))). + assumption. + apply Rmin_l. + elim n1; left; assumption. + elim n0; left; assumption. + split. + apply Ropp_lt_cancel; apply Rplus_lt_reg_r 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_r 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 R_dist in H8; unfold continuity_pt in |- *; + unfold continue_in in |- *; unfold limit1_in in |- *; + unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; + intros; elim (H8 _ H9); intros; exists (Rmin x0 (b - a)); + split. + unfold Rmin in |- *; case (Rle_dec x0 (b - a)); intro. + elim H10; intros; assumption. + change (0 < b - a) in |- *; apply Rlt_Rminus; assumption. + intros; elim H11; clear H11; intros _ H11; cut (a < x1). + intro; unfold h in |- *; case (Rle_dec x a); intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). + case (Rle_dec x1 a); intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H12)). + case (Rle_dec x b); intro. + case (Rle_dec x1 b); intro. + rewrite H6; elim H10; intros; elim r0; intro. + apply H14; split. + unfold D_x, no_cond in |- *; split. + trivial. + red in |- *; 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 in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + assumption. + rewrite H6; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + assumption. + elim n1; right; assumption. + rewrite H6 in H11; apply Ropp_lt_cancel; apply Rplus_lt_reg_r 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 in |- *; unfold continue_in in |- *; + unfold limit1_in in |- *; unfold limit_in in |- *; + simpl in |- *; unfold R_dist in |- *; intros; exists (x - b); + split. + change (0 < x - b) in |- *; apply Rlt_Rminus; assumption. + intros; elim H8; clear H8; intros. + assert (H10 : b < x0). + apply Ropp_lt_cancel; apply Rplus_lt_reg_r with x; + apply Rle_lt_trans with (Rabs (x0 - x)). + rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs. + assumption. + unfold h in |- *; case (Rle_dec x a); intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). + case (Rle_dec x b); intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H6)). + case (Rle_dec x0 a); intro. + elim (Rlt_irrefl _ (Rlt_trans _ _ _ H1 (Rlt_le_trans _ _ _ H10 r))). + case (Rle_dec x0 b); intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H10)). + unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + intros; elim H3; intros; unfold h in |- *; case (Rle_dec c a); intro. + elim r; intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 H6)). + rewrite H6; reflexivity. + case (Rle_dec c b); intro. + reflexivity. + elim n0; 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. (**********) Lemma continuity_ab_maj : - forall (f:R -> R) (a b:R), - a <= b -> - (forall c:R, a <= c <= b -> continuity_pt f c) -> + 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. -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))). -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 in |- *; 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 in |- *; rewrite <- Rplus_0_r; unfold Rminus in |- *; - 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 in |- *; intros; cut (x <= M). -intro; case (Rle_dec x (M - eps)); intro. -apply r. -elim (H9 x); unfold intersection_domain, disc, image_dir in |- *; split. -rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; rewrite Rabs_right. -apply Rplus_lt_reg_r with (x - eps); - replace (x - eps + (M - x)) with (M - eps). -replace (x - eps + eps) with x. -auto with real. -ring. -ring. -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 in |- *; intro; elim (H11 y). -unfold intersection_domain in |- *; 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 -> +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))). + 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 in |- *; 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 in |- *; rewrite <- Rplus_0_r; unfold Rminus in |- *; + 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 in |- *; intros; cut (x <= M). + intro; case (Rle_dec x (M - eps)); intro. + apply r. + elim (H9 x); unfold intersection_domain, disc, image_dir in |- *; split. + rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; rewrite Rabs_right. + apply Rplus_lt_reg_r with (x - eps); + replace (x - eps + (M - x)) with (M - eps). + replace (x - eps + eps) with x. + auto with real. + ring. + ring. + 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 in |- *; intro; elim (H11 y). + unfold intersection_domain in |- *; 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 in |- *; 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 in |- *; exists a; split. -reflexivity. -split; [ right; reflexivity | apply H ]. -unfold bound in |- *; unfold bounded in H4; elim H4; clear H4; intros m H4; - elim H4; clear H4; intros M H4; exists M; unfold is_upper_bound in |- *; - intros; elim (H4 _ H5); intros _ H6; apply H6. -apply prolongement_C0; assumption. + 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 in |- *; 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 in |- *; exists a; split. + reflexivity. + split; [ right; reflexivity | apply H ]. + unfold bound in |- *; unfold bounded in H4; elim H4; clear H4; intros m H4; + elim H4; clear H4; intros M H4; exists M; unfold is_upper_bound in |- *; + intros; elim (H4 _ H5); intros _ H6; apply H6. + apply prolongement_C0; assumption. Qed. (**********) Lemma continuity_ab_min : - forall (f:R -> R) (a b:R), - a <= b -> - (forall c:R, a <= c <= b -> continuity_pt f c) -> + 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 mx <= f c) /\ a <= mx <= b. -intros. -cut (forall c:R, a <= c <= b -> continuity_pt (- f0) c). -intro; assert (H2 := continuity_ab_maj (- f0)%F a b H H1); elim H2; - intros x0 H3; exists x0; intros; split. -intros; rewrite <- (Ropp_involutive (f0 x0)); - rewrite <- (Ropp_involutive (f0 c)); apply Ropp_le_contravar; - elim H3; intros; unfold opp_fct in H5; apply H5; apply H4. -elim H3; intros; assumption. -intros. -assert (H2 := H0 _ H1). -apply (continuity_pt_opp _ _ H2). +Proof. + intros. + cut (forall c:R, a <= c <= b -> continuity_pt (- f0) c). + intro; assert (H2 := continuity_ab_maj (- f0)%F a b H H1); elim H2; + intros x0 H3; exists x0; intros; split. + intros; rewrite <- (Ropp_involutive (f0 x0)); + rewrite <- (Ropp_involutive (f0 c)); apply Ropp_le_contravar; + elim H3; intros; unfold opp_fct in H5; apply H5; apply H4. + elim H3; intros; assumption. + intros. + assert (H2 := H0 _ H1). + apply (continuity_pt_opp _ _ H2). Qed. (********************************************************) -(* Proof of Bolzano-Weierstrass theorem *) +(** * Proof of Bolzano-Weierstrass theorem *) (********************************************************) Definition ValAdh (un:nat -> R) (x:R) : Prop := @@ -1280,66 +1319,69 @@ Definition intersection_family (f:family) (x:R) : Prop := forall y:R, ind f y -> f y x. Lemma ValAdh_un_exists : - forall (un:nat -> R) (D:=fun x:R => exists n : nat, x = INR n) - (f:= - fun x:R => - adherence + forall (un:nat -> R) (D:=fun x:R => exists n : nat, x = INR n) + (f:= + fun x:R => + adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)) - (x:R), (exists y : R, f x y) -> D x. -intros; elim H; intros; unfold f in H0; unfold adherence in H0; - unfold point_adherent in H0; - assert (H1 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0). -unfold neighbourhood, disc in |- *; exists (mkposreal _ Rlt_0_1); - unfold included in |- *; trivial. -elim (H0 _ H1); intros; unfold intersection_domain in H2; elim H2; intros; - elim H4; intros; apply H6. + (x:R), (exists y : R, f x y) -> D x. +Proof. + intros; elim H; intros; unfold f in H0; unfold adherence in H0; + unfold point_adherent in H0; + assert (H1 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0). + unfold neighbourhood, disc in |- *; exists (mkposreal _ Rlt_0_1); + unfold included in |- *; trivial. + elim (H0 _ H1); intros; unfold intersection_domain in H2; elim H2; intros; + elim H4; intros; apply H6. Qed. Definition ValAdh_un (un:nat -> R) : R -> Prop := let D := fun x:R => exists n : nat, x = INR n in - let f := - fun x:R => - adherence + let f := + fun x:R => + adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x) in - intersection_family (mkfamily D f (ValAdh_un_exists un)). + intersection_family (mkfamily D f (ValAdh_un_exists un)). Lemma ValAdh_un_prop : - forall (un:nat -> R) (x:R), ValAdh un x <-> ValAdh_un un x. -intros; split; intro. -unfold ValAdh in H; unfold ValAdh_un in |- *; - unfold intersection_family in |- *; simpl in |- *; - intros; elim H0; intros N H1; unfold adherence in |- *; - unfold point_adherent in |- *; intros; elim (H V N H2); - intros; exists (un x0); unfold intersection_domain in |- *; - elim H3; clear H3; intros; split. -assumption. -split. -exists x0; split; [ reflexivity | rewrite H1; apply (le_INR _ _ H3) ]. -exists N; assumption. -unfold ValAdh in |- *; intros; unfold ValAdh_un in H; - unfold intersection_family in H; simpl in H; - assert - (H1 : - adherence - (fun y0:R => - (exists p : nat, y0 = un p /\ INR N <= INR p) /\ - (exists n : nat, INR N = INR n)) x). -apply H; exists N; reflexivity. -unfold adherence in H1; unfold point_adherent in H1; assert (H2 := H1 _ H0); - elim H2; intros; unfold intersection_domain in H3; - elim H3; clear H3; intros; elim H4; clear H4; intros; - elim H4; clear H4; intros; elim H4; clear H4; intros; - exists x1; split. -apply (INR_le _ _ H6). -rewrite H4 in H3; apply H3. + forall (un:nat -> R) (x:R), ValAdh un x <-> ValAdh_un un x. +Proof. + intros; split; intro. + unfold ValAdh in H; unfold ValAdh_un in |- *; + unfold intersection_family in |- *; simpl in |- *; + intros; elim H0; intros N H1; unfold adherence in |- *; + unfold point_adherent in |- *; intros; elim (H V N H2); + intros; exists (un x0); unfold intersection_domain in |- *; + elim H3; clear H3; intros; split. + assumption. + split. + exists x0; split; [ reflexivity | rewrite H1; apply (le_INR _ _ H3) ]. + exists N; assumption. + unfold ValAdh in |- *; intros; unfold ValAdh_un in H; + unfold intersection_family in H; simpl in H; + assert + (H1 : + adherence + (fun y0:R => + (exists p : nat, y0 = un p /\ INR N <= INR p) /\ + (exists n : nat, INR N = INR n)) x). + apply H; exists N; reflexivity. + unfold adherence in H1; unfold point_adherent in H1; assert (H2 := H1 _ H0); + elim H2; intros; unfold intersection_domain in H3; + elim H3; clear H3; intros; elim H4; clear H4; intros; + elim H4; clear H4; intros; elim H4; clear H4; intros; + exists x1; split. + apply (INR_le _ _ H6). + rewrite H4 in H3; apply H3. Qed. Lemma adherence_P4 : - forall F G:R -> Prop, included F G -> included (adherence F) (adherence G). -unfold adherence, included in |- *; unfold point_adherent in |- *; intros; - elim (H0 _ H1); unfold intersection_domain in |- *; - intros; elim H2; clear H2; intros; exists x0; split; - [ assumption | apply (H _ H3) ]. + forall F G:R -> Prop, included F G -> included (adherence F) (adherence G). +Proof. + unfold adherence, included in |- *; unfold point_adherent in |- *; intros; + elim (H0 _ H1); unfold intersection_domain in |- *; + intros; elim H2; clear H2; intros; exists x0; split; + [ assumption | apply (H _ H3) ]. Qed. Definition family_closed_set (f:family) : Prop := @@ -1355,471 +1397,476 @@ Definition intersection_vide_finite_in (D:R -> Prop) (**********) Lemma compact_P6 : - forall X:R -> Prop, - compact X -> - (exists z : R, X z) -> - forall g:family, - family_closed_set g -> - intersection_vide_in X g -> + forall X:R -> Prop, + compact X -> + (exists z : R, X z) -> + forall g:family, + family_closed_set g -> + intersection_vide_in X g -> exists D : R -> Prop, intersection_vide_finite_in X (subfamily g D). -intros X H Hyp g H0 H1. -set (D' := ind g). -set (f' := fun x y:R => complementary (g x) y /\ D' x). -assert (H2 : forall x:R, (exists y : R, f' x y) -> D' x). -intros; elim H2; intros; unfold f' in H3; elim H3; intros; assumption. -set (f0 := mkfamily D' f' H2). -unfold compact in H; assert (H3 : covering_open_set X f0). -unfold covering_open_set in |- *; split. -unfold covering in |- *; intros; unfold intersection_vide_in in H1; - elim (H1 x); intros; unfold intersection_family in H5; - assert - (H6 := not_ex_all_not _ (fun y:R => forall y0:R, ind g y0 -> g y0 y) H5 x); - assert (H7 := not_all_ex_not _ (fun y0:R => ind g y0 -> g y0 x) H6); - elim H7; intros; exists x0; elim (imply_to_and _ _ H8); - intros; unfold f0 in |- *; simpl in |- *; unfold f' in |- *; - split; [ apply H10 | apply H9 ]. -unfold family_open_set in |- *; intro; elim (classic (D' x)); intro. -apply open_set_P6 with (complementary (g x)). -unfold family_closed_set in H0; unfold closed_set in H0; apply H0. -unfold f0 in |- *; simpl in |- *; unfold f' in |- *; unfold eq_Dom in |- *; - split. -unfold included in |- *; intros; split; [ apply H4 | apply H3 ]. -unfold included in |- *; intros; elim H4; intros; assumption. -apply open_set_P6 with (fun _:R => False). -apply open_set_P4. -unfold eq_Dom in |- *; unfold included in |- *; split; intros; - [ elim H4 - | simpl in H4; unfold f' in H4; elim H4; intros; elim H3; assumption ]. -elim (H _ H3); intros SF H4; exists SF; - unfold intersection_vide_finite_in in |- *; split. -unfold intersection_vide_in in |- *; simpl in |- *; intros; split. -intros; unfold included in |- *; intros; unfold intersection_vide_in in H1; - elim (H1 x); intros; elim H6; intros; apply H7. -unfold intersection_domain in H5; elim H5; intros; assumption. -assumption. -elim (classic (exists y : R, intersection_domain (ind g) SF y)); intro Hyp'. -red in |- *; intro; elim H5; intros; unfold intersection_family in H6; - simpl in H6. -cut (X x0). -intro; unfold covering_finite in H4; elim H4; clear H4; intros H4 _; - unfold covering in H4; elim (H4 x0 H7); intros; simpl in H8; - unfold intersection_domain in H6; cut (ind g x1 /\ SF x1). -intro; assert (H10 := H6 x1 H9); elim H10; clear H10; intros H10 _; elim H8; - clear H8; intros H8 _; unfold f' in H8; unfold complementary in H8; - elim H8; clear H8; intros H8 _; elim H8; assumption. -split. -apply (cond_fam f0). -exists x0; elim H8; intros; assumption. -elim H8; intros; assumption. -unfold intersection_vide_in in H1; elim Hyp'; intros; assert (H8 := H6 _ H7); - elim H8; intros; cut (ind g x1). -intro; elim (H1 x1); intros; apply H12. -apply H11. -apply H9. -apply (cond_fam g); exists x0; assumption. -unfold covering_finite in H4; elim H4; clear H4; intros H4 _; - cut (exists z : R, X z). -intro; elim H5; clear H5; intros; unfold covering in H4; elim (H4 x0 H5); - intros; simpl in H6; elim Hyp'; exists x1; elim H6; - intros; unfold intersection_domain in |- *; split. -apply (cond_fam f0); exists x0; apply H7. -apply H8. -apply Hyp. -unfold covering_finite in H4; elim H4; clear H4; intros; - unfold family_finite in H5; unfold domain_finite in H5; - unfold family_finite in |- *; unfold domain_finite in |- *; - elim H5; clear H5; intros l H5; exists l; intro; elim (H5 x); - intros; split; intro; - [ apply H6; simpl in |- *; simpl in H8; apply H8 | apply (H7 H8) ]. +Proof. + intros X H Hyp g H0 H1. + set (D' := ind g). + set (f' := fun x y:R => complementary (g x) y /\ D' x). + assert (H2 : forall x:R, (exists y : R, f' x y) -> D' x). + intros; elim H2; intros; unfold f' in H3; elim H3; intros; assumption. + set (f0 := mkfamily D' f' H2). + unfold compact in H; assert (H3 : covering_open_set X f0). + unfold covering_open_set in |- *; split. + unfold covering in |- *; intros; unfold intersection_vide_in in H1; + elim (H1 x); intros; unfold intersection_family in H5; + assert + (H6 := not_ex_all_not _ (fun y:R => forall y0:R, ind g y0 -> g y0 y) H5 x); + assert (H7 := not_all_ex_not _ (fun y0:R => ind g y0 -> g y0 x) H6); + elim H7; intros; exists x0; elim (imply_to_and _ _ H8); + intros; unfold f0 in |- *; simpl in |- *; unfold f' in |- *; + split; [ apply H10 | apply H9 ]. + unfold family_open_set in |- *; intro; elim (classic (D' x)); intro. + apply open_set_P6 with (complementary (g x)). + unfold family_closed_set in H0; unfold closed_set in H0; apply H0. + unfold f0 in |- *; simpl in |- *; unfold f' in |- *; unfold eq_Dom in |- *; + split. + unfold included in |- *; intros; split; [ apply H4 | apply H3 ]. + unfold included in |- *; intros; elim H4; intros; assumption. + apply open_set_P6 with (fun _:R => False). + apply open_set_P4. + unfold eq_Dom in |- *; unfold included in |- *; split; intros; + [ elim H4 + | simpl in H4; unfold f' in H4; elim H4; intros; elim H3; assumption ]. + elim (H _ H3); intros SF H4; exists SF; + unfold intersection_vide_finite_in in |- *; split. + unfold intersection_vide_in in |- *; simpl in |- *; intros; split. + intros; unfold included in |- *; intros; unfold intersection_vide_in in H1; + elim (H1 x); intros; elim H6; intros; apply H7. + unfold intersection_domain in H5; elim H5; intros; assumption. + assumption. + elim (classic (exists y : R, intersection_domain (ind g) SF y)); intro Hyp'. + red in |- *; intro; elim H5; intros; unfold intersection_family in H6; + simpl in H6. + cut (X x0). + intro; unfold covering_finite in H4; elim H4; clear H4; intros H4 _; + unfold covering in H4; elim (H4 x0 H7); intros; simpl in H8; + unfold intersection_domain in H6; cut (ind g x1 /\ SF x1). + intro; assert (H10 := H6 x1 H9); elim H10; clear H10; intros H10 _; elim H8; + clear H8; intros H8 _; unfold f' in H8; unfold complementary in H8; + elim H8; clear H8; intros H8 _; elim H8; assumption. + split. + apply (cond_fam f0). + exists x0; elim H8; intros; assumption. + elim H8; intros; assumption. + unfold intersection_vide_in in H1; elim Hyp'; intros; assert (H8 := H6 _ H7); + elim H8; intros; cut (ind g x1). + intro; elim (H1 x1); intros; apply H12. + apply H11. + apply H9. + apply (cond_fam g); exists x0; assumption. + unfold covering_finite in H4; elim H4; clear H4; intros H4 _; + cut (exists z : R, X z). + intro; elim H5; clear H5; intros; unfold covering in H4; elim (H4 x0 H5); + intros; simpl in H6; elim Hyp'; exists x1; elim H6; + intros; unfold intersection_domain in |- *; split. + apply (cond_fam f0); exists x0; apply H7. + apply H8. + apply Hyp. + unfold covering_finite in H4; elim H4; clear H4; intros; + unfold family_finite in H5; unfold domain_finite in H5; + unfold family_finite in |- *; unfold domain_finite in |- *; + elim H5; clear H5; intros l H5; exists l; intro; elim (H5 x); + intros; split; intro; + [ apply H6; simpl in |- *; simpl in H8; apply H8 | apply (H7 H8) ]. Qed. Theorem Bolzano_Weierstrass : - forall (un:nat -> R) (X:R -> Prop), - compact X -> (forall n:nat, X (un n)) -> exists l : R, ValAdh un l. -intros; cut (exists l : R, ValAdh_un un l). -intro; elim H1; intros; exists x; elim (ValAdh_un_prop un x); intros; - apply (H4 H2). -assert (H1 : exists z : R, X z). -exists (un 0%nat); apply H0. -set (D := fun x:R => exists n : nat, x = INR n). -set - (g := - fun x:R => - adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)). -assert (H2 : forall x:R, (exists y : R, g x y) -> D x). -intros; elim H2; intros; unfold g in H3; unfold adherence in H3; - unfold point_adherent in H3. -assert (H4 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0). -unfold neighbourhood in |- *; exists (mkposreal _ Rlt_0_1); - unfold included in |- *; trivial. -elim (H3 _ H4); intros; unfold intersection_domain in H5; decompose [and] H5; - assumption. -set (f0 := mkfamily D g H2). -assert (H3 := compact_P6 X H H1 f0). -elim (classic (exists l : R, ValAdh_un un l)); intro. -assumption. -cut (family_closed_set f0). -intro; cut (intersection_vide_in X f0). -intro; assert (H7 := H3 H5 H6). -elim H7; intros SF H8; unfold intersection_vide_finite_in in H8; elim H8; - clear H8; intros; unfold intersection_vide_in in H8; - elim (H8 0); intros _ H10; elim H10; unfold family_finite in H9; - unfold domain_finite in H9; elim H9; clear H9; intros l H9; - set (r := MaxRlist l); cut (D r). -intro; unfold D in H11; elim H11; intros; exists (un x); - unfold intersection_family in |- *; simpl in |- *; - unfold intersection_domain in |- *; intros; split. -unfold g in |- *; apply adherence_P1; split. -exists x; split; - [ reflexivity - | rewrite <- H12; unfold r in |- *; apply MaxRlist_P1; elim (H9 y); intros; - apply H14; simpl in |- *; apply H13 ]. -elim H13; intros; assumption. -elim H13; intros; assumption. -elim (H9 r); intros. -simpl in H12; unfold intersection_domain in H12; cut (In r l). -intro; elim (H12 H13); intros; assumption. -unfold r in |- *; apply MaxRlist_P2; - cut (exists z : R, intersection_domain (ind f0) SF z). -intro; elim H13; intros; elim (H9 x); intros; simpl in H15; - assert (H17 := H15 H14); exists x; apply H17. -elim (classic (exists z : R, intersection_domain (ind f0) SF z)); intro. -assumption. -elim (H8 0); intros _ H14; elim H1; intros; - assert - (H16 := - not_ex_all_not _ (fun y:R => intersection_family (subfamily f0 SF) y) H14); - assert - (H17 := - not_ex_all_not _ (fun z:R => intersection_domain (ind f0) SF z) H13); - assert (H18 := H16 x); unfold intersection_family in H18; - simpl in H18; - assert - (H19 := - not_all_ex_not _ (fun y:R => intersection_domain D SF y -> g y x /\ SF y) - H18); elim H19; intros; assert (H21 := imply_to_and _ _ H20); - elim (H17 x0); elim H21; intros; assumption. -unfold intersection_vide_in in |- *; intros; split. -intro; simpl in H6; unfold f0 in |- *; simpl in |- *; unfold g in |- *; - apply included_trans with (adherence X). -apply adherence_P4. -unfold included in |- *; intros; elim H7; intros; elim H8; intros; elim H10; - intros; rewrite H11; apply H0. -apply adherence_P2; apply compact_P2; assumption. -apply H4. -unfold family_closed_set in |- *; unfold f0 in |- *; simpl in |- *; - unfold g in |- *; intro; apply adherence_P3. + forall (un:nat -> R) (X:R -> Prop), + compact X -> (forall n:nat, X (un n)) -> exists l : R, ValAdh un l. +Proof. + intros; cut (exists l : R, ValAdh_un un l). + intro; elim H1; intros; exists x; elim (ValAdh_un_prop un x); intros; + apply (H4 H2). + assert (H1 : exists z : R, X z). + exists (un 0%nat); apply H0. + set (D := fun x:R => exists n : nat, x = INR n). + set + (g := + fun x:R => + adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)). + assert (H2 : forall x:R, (exists y : R, g x y) -> D x). + intros; elim H2; intros; unfold g in H3; unfold adherence in H3; + unfold point_adherent in H3. + assert (H4 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0). + unfold neighbourhood in |- *; exists (mkposreal _ Rlt_0_1); + unfold included in |- *; trivial. + elim (H3 _ H4); intros; unfold intersection_domain in H5; decompose [and] H5; + assumption. + set (f0 := mkfamily D g H2). + assert (H3 := compact_P6 X H H1 f0). + elim (classic (exists l : R, ValAdh_un un l)); intro. + assumption. + cut (family_closed_set f0). + intro; cut (intersection_vide_in X f0). + intro; assert (H7 := H3 H5 H6). + elim H7; intros SF H8; unfold intersection_vide_finite_in in H8; elim H8; + clear H8; intros; unfold intersection_vide_in in H8; + elim (H8 0); intros _ H10; elim H10; unfold family_finite in H9; + unfold domain_finite in H9; elim H9; clear H9; intros l H9; + set (r := MaxRlist l); cut (D r). + intro; unfold D in H11; elim H11; intros; exists (un x); + unfold intersection_family in |- *; simpl in |- *; + unfold intersection_domain in |- *; intros; split. + unfold g in |- *; apply adherence_P1; split. + exists x; split; + [ reflexivity + | rewrite <- H12; unfold r in |- *; apply MaxRlist_P1; elim (H9 y); intros; + apply H14; simpl in |- *; apply H13 ]. + elim H13; intros; assumption. + elim H13; intros; assumption. + elim (H9 r); intros. + simpl in H12; unfold intersection_domain in H12; cut (In r l). + intro; elim (H12 H13); intros; assumption. + unfold r in |- *; apply MaxRlist_P2; + cut (exists z : R, intersection_domain (ind f0) SF z). + intro; elim H13; intros; elim (H9 x); intros; simpl in H15; + assert (H17 := H15 H14); exists x; apply H17. + elim (classic (exists z : R, intersection_domain (ind f0) SF z)); intro. + assumption. + elim (H8 0); intros _ H14; elim H1; intros; + assert + (H16 := + not_ex_all_not _ (fun y:R => intersection_family (subfamily f0 SF) y) H14); + assert + (H17 := + not_ex_all_not _ (fun z:R => intersection_domain (ind f0) SF z) H13); + assert (H18 := H16 x); unfold intersection_family in H18; + simpl in H18; + assert + (H19 := + not_all_ex_not _ (fun y:R => intersection_domain D SF y -> g y x /\ SF y) + H18); elim H19; intros; assert (H21 := imply_to_and _ _ H20); + elim (H17 x0); elim H21; intros; assumption. + unfold intersection_vide_in in |- *; intros; split. + intro; simpl in H6; unfold f0 in |- *; simpl in |- *; unfold g in |- *; + apply included_trans with (adherence X). + apply adherence_P4. + unfold included in |- *; intros; elim H7; intros; elim H8; intros; elim H10; + intros; rewrite H11; apply H0. + apply adherence_P2; apply compact_P2; assumption. + apply H4. + unfold family_closed_set in |- *; unfold f0 in |- *; simpl in |- *; + unfold g in |- *; intro; apply adherence_P3. Qed. (********************************************************) -(* Proof of Heine's theorem *) +(** * Proof of Heine's theorem *) (********************************************************) Definition uniform_continuity (f:R -> R) (X:R -> Prop) : Prop := forall eps:posreal, - exists delta : posreal, + exists delta : posreal, (forall x y:R, - X x -> X y -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps). + X x -> X y -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps). Lemma is_lub_u : - forall (E:R -> Prop) (x y:R), is_lub E x -> is_lub E y -> x = y. -unfold is_lub in |- *; intros; elim H; elim H0; intros; apply Rle_antisym; - [ apply (H4 _ H1) | apply (H2 _ H3) ]. + forall (E:R -> Prop) (x y:R), is_lub E x -> is_lub E y -> x = y. +Proof. + unfold is_lub in |- *; intros; elim H; elim H0; intros; apply Rle_antisym; + [ apply (H4 _ H1) | apply (H2 _ H3) ]. Qed. Lemma domain_P1 : - forall X:R -> Prop, - ~ (exists y : R, X y) \/ - (exists y : R, X y /\ (forall x:R, X x -> x = y)) \/ - (exists x : R, (exists y : R, X x /\ X y /\ x <> y)). -intro; elim (classic (exists y : R, X y)); intro. -right; elim H; intros; elim (classic (exists y : R, X y /\ y <> x)); intro. -right; elim H1; intros; elim H2; intros; exists x; exists x0; intros. -split; - [ assumption - | split; [ assumption | apply (sym_not_eq (A:=R)); assumption ] ]. -left; exists x; split. -assumption. -intros; case (Req_dec x0 x); intro. -assumption. -elim H1; exists x0; split; assumption. -left; assumption. + forall X:R -> Prop, + ~ (exists y : R, X y) \/ + (exists y : R, X y /\ (forall x:R, X x -> x = y)) \/ + (exists x : R, (exists y : R, X x /\ X y /\ x <> y)). +Proof. + intro; elim (classic (exists y : R, X y)); intro. + right; elim H; intros; elim (classic (exists y : R, X y /\ y <> x)); intro. + right; elim H1; intros; elim H2; intros; exists x; exists x0; intros. + split; + [ assumption + | split; [ assumption | apply (sym_not_eq (A:=R)); assumption ] ]. + left; exists x; split. + assumption. + intros; case (Req_dec x0 x); intro. + assumption. + elim H1; exists x0; split; assumption. + left; assumption. Qed. Theorem Heine : - forall (f:R -> R) (X:R -> Prop), - compact X -> - (forall x:R, X x -> continuity_pt f x) -> uniform_continuity f X. -intros f0 X H0 H; elim (domain_P1 X); intro Hyp. + forall (f:R -> R) (X:R -> Prop), + compact X -> + (forall x:R, X x -> continuity_pt f x) -> uniform_continuity f X. +Proof. + intros f0 X H0 H; elim (domain_P1 X); intro Hyp. (* X est vide *) -unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); - intros; elim Hyp; exists x; assumption. -elim Hyp; clear Hyp; intro Hyp. + unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); + intros; elim Hyp; exists x; assumption. + elim Hyp; clear Hyp; intro Hyp. (* X possède un seul élément *) -unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); - intros; elim Hyp; clear Hyp; intros; elim H4; clear H4; - intros; assert (H6 := H5 _ H1); assert (H7 := H5 _ H2); - rewrite H6; rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; - rewrite Rabs_R0; apply (cond_pos eps). + unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); + intros; elim Hyp; clear Hyp; intros; elim H4; clear H4; + intros; assert (H6 := H5 _ H1); assert (H7 := H5 _ H2); + rewrite H6; rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; + rewrite Rabs_R0; apply (cond_pos eps). (* X possède au moins deux éléments distincts *) -assert - (X_enc : - exists m : R, (exists M : R, (forall x:R, X x -> m <= x <= M) /\ m < M)). -assert (H1 := compact_P1 X H0); unfold bounded in H1; elim H1; intros; - elim H2; intros; exists x; exists x0; split. -apply H3. -elim Hyp; intros; elim H4; intros; decompose [and] H5; - assert (H10 := H3 _ H6); assert (H11 := H3 _ H8); - elim H10; intros; elim H11; intros; case (total_order_T x x0); - intro. -elim s; intro. -assumption. -rewrite b in H13; rewrite b in H7; elim H9; apply Rle_antisym; - apply Rle_trans with x0; assumption. -elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H13 H14) r)). -elim X_enc; clear X_enc; intros m X_enc; elim X_enc; clear X_enc; - intros M X_enc; elim X_enc; clear X_enc Hyp; intros X_enc Hyp; - unfold uniform_continuity in |- *; intro; - assert (H1 : forall t:posreal, 0 < t / 2). -intro; unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply (cond_pos t) | apply Rinv_0_lt_compat; prove_sup0 ]. -set - (g := - fun x y:R => - X x /\ - (exists del : posreal, - (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ - is_lub - (fun zeta:R => + assert + (X_enc : + exists m : R, (exists M : R, (forall x:R, X x -> m <= x <= M) /\ m < M)). + assert (H1 := compact_P1 X H0); unfold bounded in H1; elim H1; intros; + elim H2; intros; exists x; exists x0; split. + apply H3. + elim Hyp; intros; elim H4; intros; decompose [and] H5; + assert (H10 := H3 _ H6); assert (H11 := H3 _ H8); + elim H10; intros; elim H11; intros; case (total_order_T x x0); + intro. + elim s; intro. + assumption. + rewrite b in H13; rewrite b in H7; elim H9; apply Rle_antisym; + apply Rle_trans with x0; assumption. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H13 H14) r)). + elim X_enc; clear X_enc; intros m X_enc; elim X_enc; clear X_enc; + intros M X_enc; elim X_enc; clear X_enc Hyp; intros X_enc Hyp; + unfold uniform_continuity in |- *; intro; + assert (H1 : forall t:posreal, 0 < t / 2). + intro; unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply (cond_pos t) | apply Rinv_0_lt_compat; prove_sup0 ]. + set + (g := + fun x y:R => + X x /\ + (exists del : posreal, + (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ + is_lub + (fun zeta:R => 0 < zeta <= M - m /\ (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)) - del /\ disc x (mkposreal (del / 2) (H1 del)) y)). -assert (H2 : forall x:R, (exists y : R, g x y) -> X x). -intros; elim H2; intros; unfold g in H3; elim H3; clear H3; intros H3 _; - apply H3. -set (f' := mkfamily X g H2); unfold compact in H0; - assert (H3 : covering_open_set X f'). -unfold covering_open_set in |- *; split. -unfold covering in |- *; intros; exists x; simpl in |- *; unfold g in |- *; - split. -assumption. -assert (H4 := H _ H3); unfold continuity_pt in H4; unfold continue_in in H4; - unfold limit1_in in H4; unfold limit_in in H4; simpl in H4; - unfold R_dist in H4; elim (H4 (eps / 2) (H1 eps)); - intros; - set - (E := - fun zeta:R => - 0 < zeta <= M - m /\ - (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)); - assert (H6 : bound E). -unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *; - unfold E in |- *; intros; elim H6; clear H6; intros H6 _; - elim H6; clear H6; intros _ H6; apply H6. -assert (H7 : exists x : R, E x). -elim H5; clear H5; intros; exists (Rmin x0 (M - m)); unfold E in |- *; intros; - split. -split. -unfold Rmin in |- *; case (Rle_dec x0 (M - m)); intro. -apply H5. -apply Rlt_Rminus; apply Hyp. -apply Rmin_r. -intros; case (Req_dec x z); intro. -rewrite H9; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; - apply (H1 eps). -apply H7; split. -unfold D_x, no_cond in |- *; split; [ trivial | assumption ]. -apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H8 | apply Rmin_l ]. -assert (H8 := completeness _ H6 H7); elim H8; clear H8; intros; - cut (0 < x1 <= M - m). -intro; elim H8; clear H8; intros; exists (mkposreal _ H8); split. -intros; cut (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp). -intros; elim H11; intros; elim H12; clear H12; intros; unfold E in H13; - elim H13; intros; apply H15. -elim H12; intros; assumption. -elim (classic (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp)); intro. -assumption. -assert - (H12 := - not_ex_all_not _ (fun alp:R => Rabs (z - x) < alp <= x1 /\ E alp) H11); - unfold is_lub in p; elim p; intros; cut (is_upper_bound E (Rabs (z - x))). -intro; assert (H16 := H14 _ H15); - elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H10 H16)). -unfold is_upper_bound in |- *; intros; unfold is_upper_bound in H13; - assert (H16 := H13 _ H15); case (Rle_dec x2 (Rabs (z - x))); - intro. -assumption. -elim (H12 x2); split; [ split; [ auto with real | assumption ] | assumption ]. -split. -apply p. -unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; - rewrite Rabs_R0; simpl in |- *; unfold Rdiv in |- *; - apply Rmult_lt_0_compat; [ apply H8 | apply Rinv_0_lt_compat; prove_sup0 ]. -elim H7; intros; unfold E in H8; elim H8; intros H9 _; elim H9; intros H10 _; - unfold is_lub in p; elim p; intros; unfold is_upper_bound in H12; - unfold is_upper_bound in H11; split. -apply Rlt_le_trans with x2; [ assumption | apply (H11 _ H8) ]. -apply H12; intros; unfold E in H13; elim H13; intros; elim H14; intros; - assumption. -unfold family_open_set in |- *; intro; simpl in |- *; elim (classic (X x)); - intro. -unfold g in |- *; unfold open_set in |- *; intros; elim H4; clear H4; - intros _ H4; elim H4; clear H4; intros; elim H4; clear H4; - intros; unfold neighbourhood in |- *; case (Req_dec x x0); - intro. -exists (mkposreal _ (H1 x1)); rewrite <- H6; unfold included in |- *; intros; - split. -assumption. -exists x1; split. -apply H4. -split. -elim H5; intros; apply H8. -apply H7. -set (d := x1 / 2 - Rabs (x0 - x)); assert (H7 : 0 < d). -unfold d in |- *; apply Rlt_Rminus; elim H5; clear H5; intros; - unfold disc in H7; apply H7. -exists (mkposreal _ H7); unfold included in |- *; intros; split. -assumption. -exists x1; split. -apply H4. -elim H5; intros; split. -assumption. -unfold disc in H8; simpl in H8; unfold disc in |- *; simpl in |- *; - unfold disc in H10; simpl in H10; - apply Rle_lt_trans with (Rabs (x2 - x0) + Rabs (x0 - x)). -replace (x2 - x) with (x2 - x0 + (x0 - x)); [ apply Rabs_triang | ring ]. -replace (x1 / 2) with (d + Rabs (x0 - x)); [ idtac | unfold d in |- *; ring ]. -do 2 rewrite <- (Rplus_comm (Rabs (x0 - x))); apply Rplus_lt_compat_l; - apply H8. -apply open_set_P6 with (fun _:R => False). -apply open_set_P4. -unfold eq_Dom in |- *; unfold included in |- *; intros; split. -intros; elim H4. -intros; unfold g in H4; elim H4; clear H4; intros H4 _; elim H3; apply H4. -elim (H0 _ H3); intros DF H4; unfold covering_finite in H4; elim H4; clear H4; - intros; unfold family_finite in H5; unfold domain_finite in H5; - unfold covering in H4; simpl in H4; simpl in H5; elim H5; - clear H5; intros l H5; unfold intersection_domain in H5; - cut - (forall x:R, - In x l -> - exists del : R, - 0 < del /\ - (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ - included (g x) (fun z:R => Rabs (z - x) < del / 2)). -intros; - assert - (H7 := - Rlist_P1 l - (fun x del:R => - 0 < del /\ - (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ - included (g x) (fun z:R => Rabs (z - x) < del / 2)) H6); - elim H7; clear H7; intros l' H7; elim H7; clear H7; - intros; set (D := MinRlist l'); cut (0 < D / 2). -intro; exists (mkposreal _ H9); intros; assert (H13 := H4 _ H10); elim H13; - clear H13; intros xi H13; assert (H14 : In xi l). -unfold g in H13; decompose [and] H13; elim (H5 xi); intros; apply H14; split; - assumption. -elim (pos_Rl_P2 l xi); intros H15 _; elim (H15 H14); intros i H16; elim H16; - intros; apply Rle_lt_trans with (Rabs (f0 x - f0 xi) + Rabs (f0 xi - f0 y)). -replace (f0 x - f0 y) with (f0 x - f0 xi + (f0 xi - f0 y)); - [ apply Rabs_triang | ring ]. -rewrite (double_var eps); apply Rplus_lt_compat. -assert (H19 := H8 i H17); elim H19; clear H19; intros; rewrite <- H18 in H20; - elim H20; clear H20; intros; apply H20; unfold included in H21; - apply Rlt_trans with (pos_Rl l' i / 2). -apply H21. -elim H13; clear H13; intros; assumption. -unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2. -prove_sup0. -rewrite Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_r; pattern (pos_Rl l' i) at 1 in |- *; rewrite <- Rplus_0_r; - rewrite double; apply Rplus_lt_compat_l; apply H19. -discrR. -assert (H19 := H8 i H17); elim H19; clear H19; intros; rewrite <- H18 in H20; - elim H20; clear H20; intros; rewrite <- Rabs_Ropp; - rewrite Ropp_minus_distr; apply H20; unfold included in H21; - elim H13; intros; assert (H24 := H21 x H22); - apply Rle_lt_trans with (Rabs (y - x) + Rabs (x - xi)). -replace (y - xi) with (y - x + (x - xi)); [ apply Rabs_triang | ring ]. -rewrite (double_var (pos_Rl l' i)); apply Rplus_lt_compat. -apply Rlt_le_trans with (D / 2). -rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H12. -unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ 2)); - apply Rmult_le_compat_l. -left; apply Rinv_0_lt_compat; prove_sup0. -unfold D in |- *; apply MinRlist_P1; elim (pos_Rl_P2 l' (pos_Rl l' i)); - intros; apply H26; exists i; split; - [ rewrite <- H7; assumption | reflexivity ]. -assumption. -unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ unfold D in |- *; apply MinRlist_P2; intros; elim (pos_Rl_P2 l' y); intros; - elim (H10 H9); intros; elim H12; intros; rewrite H14; - rewrite <- H7 in H13; elim (H8 x H13); intros; - apply H15 - | apply Rinv_0_lt_compat; prove_sup0 ]. -intros; elim (H5 x); intros; elim (H8 H6); intros; - set - (E := - fun zeta:R => - 0 < zeta <= M - m /\ - (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)); - assert (H11 : bound E). -unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *; - unfold E in |- *; intros; elim H11; clear H11; intros H11 _; - elim H11; clear H11; intros _ H11; apply H11. -assert (H12 : exists x : R, E x). -assert (H13 := H _ H9); unfold continuity_pt in H13; - unfold continue_in in H13; unfold limit1_in in H13; - unfold limit_in in H13; simpl in H13; unfold R_dist in H13; - elim (H13 _ (H1 eps)); intros; elim H12; clear H12; - intros; exists (Rmin x0 (M - m)); unfold E in |- *; - intros; split. -split; - [ unfold Rmin in |- *; case (Rle_dec x0 (M - m)); intro; - [ apply H12 | apply Rlt_Rminus; apply Hyp ] - | apply Rmin_r ]. -intros; case (Req_dec x z); intro. -rewrite H16; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; - apply (H1 eps). -apply H14; split; - [ unfold D_x, no_cond in |- *; split; [ trivial | assumption ] - | apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H15 | apply Rmin_l ] ]. -assert (H13 := completeness _ H11 H12); elim H13; clear H13; intros; - cut (0 < x0 <= M - m). -intro; elim H13; clear H13; intros; exists x0; split. -assumption. -split. -intros; cut (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp). -intros; elim H16; intros; elim H17; clear H17; intros; unfold E in H18; - elim H18; intros; apply H20; elim H17; intros; assumption. -elim (classic (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp)); intro. -assumption. -assert - (H17 := - not_ex_all_not _ (fun alp:R => Rabs (z - x) < alp <= x0 /\ E alp) H16); - unfold is_lub in p; elim p; intros; cut (is_upper_bound E (Rabs (z - x))). -intro; assert (H21 := H19 _ H20); - elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H15 H21)). -unfold is_upper_bound in |- *; intros; unfold is_upper_bound in H18; - assert (H21 := H18 _ H20); case (Rle_dec x1 (Rabs (z - x))); - intro. -assumption. -elim (H17 x1); split. -split; [ auto with real | assumption ]. -assumption. -unfold included, g in |- *; intros; elim H15; intros; elim H17; intros; - decompose [and] H18; cut (x0 = x2). -intro; rewrite H20; apply H22. -unfold E in p; eapply is_lub_u. -apply p. -apply H21. -elim H12; intros; unfold E in H13; elim H13; intros H14 _; elim H14; - intros H15 _; unfold is_lub in p; elim p; intros; - unfold is_upper_bound in H16; unfold is_upper_bound in H17; - split. -apply Rlt_le_trans with x1; [ assumption | apply (H16 _ H13) ]. -apply H17; intros; unfold E in H18; elim H18; intros; elim H19; intros; - assumption. + del /\ disc x (mkposreal (del / 2) (H1 del)) y)). + assert (H2 : forall x:R, (exists y : R, g x y) -> X x). + intros; elim H2; intros; unfold g in H3; elim H3; clear H3; intros H3 _; + apply H3. + set (f' := mkfamily X g H2); unfold compact in H0; + assert (H3 : covering_open_set X f'). + unfold covering_open_set in |- *; split. + unfold covering in |- *; intros; exists x; simpl in |- *; unfold g in |- *; + split. + assumption. + assert (H4 := H _ H3); unfold continuity_pt in H4; unfold continue_in in H4; + unfold limit1_in in H4; unfold limit_in in H4; simpl in H4; + unfold R_dist in H4; elim (H4 (eps / 2) (H1 eps)); + intros; + set + (E := + fun zeta:R => + 0 < zeta <= M - m /\ + (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)); + assert (H6 : bound E). + unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *; + unfold E in |- *; intros; elim H6; clear H6; intros H6 _; + elim H6; clear H6; intros _ H6; apply H6. + assert (H7 : exists x : R, E x). + elim H5; clear H5; intros; exists (Rmin x0 (M - m)); unfold E in |- *; intros; + split. + split. + unfold Rmin in |- *; case (Rle_dec x0 (M - m)); intro. + apply H5. + apply Rlt_Rminus; apply Hyp. + apply Rmin_r. + intros; case (Req_dec x z); intro. + rewrite H9; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + apply (H1 eps). + apply H7; split. + unfold D_x, no_cond in |- *; split; [ trivial | assumption ]. + apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H8 | apply Rmin_l ]. + assert (H8 := completeness _ H6 H7); elim H8; clear H8; intros; + cut (0 < x1 <= M - m). + intro; elim H8; clear H8; intros; exists (mkposreal _ H8); split. + intros; cut (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp). + intros; elim H11; intros; elim H12; clear H12; intros; unfold E in H13; + elim H13; intros; apply H15. + elim H12; intros; assumption. + elim (classic (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp)); intro. + assumption. + assert + (H12 := + not_ex_all_not _ (fun alp:R => Rabs (z - x) < alp <= x1 /\ E alp) H11); + unfold is_lub in p; elim p; intros; cut (is_upper_bound E (Rabs (z - x))). + intro; assert (H16 := H14 _ H15); + elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H10 H16)). + unfold is_upper_bound in |- *; intros; unfold is_upper_bound in H13; + assert (H16 := H13 _ H15); case (Rle_dec x2 (Rabs (z - x))); + intro. + assumption. + elim (H12 x2); split; [ split; [ auto with real | assumption ] | assumption ]. + split. + apply p. + unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; + rewrite Rabs_R0; simpl in |- *; unfold Rdiv in |- *; + apply Rmult_lt_0_compat; [ apply H8 | apply Rinv_0_lt_compat; prove_sup0 ]. + elim H7; intros; unfold E in H8; elim H8; intros H9 _; elim H9; intros H10 _; + unfold is_lub in p; elim p; intros; unfold is_upper_bound in H12; + unfold is_upper_bound in H11; split. + apply Rlt_le_trans with x2; [ assumption | apply (H11 _ H8) ]. + apply H12; intros; unfold E in H13; elim H13; intros; elim H14; intros; + assumption. + unfold family_open_set in |- *; intro; simpl in |- *; elim (classic (X x)); + intro. + unfold g in |- *; unfold open_set in |- *; intros; elim H4; clear H4; + intros _ H4; elim H4; clear H4; intros; elim H4; clear H4; + intros; unfold neighbourhood in |- *; case (Req_dec x x0); + intro. + exists (mkposreal _ (H1 x1)); rewrite <- H6; unfold included in |- *; intros; + split. + assumption. + exists x1; split. + apply H4. + split. + elim H5; intros; apply H8. + apply H7. + set (d := x1 / 2 - Rabs (x0 - x)); assert (H7 : 0 < d). + unfold d in |- *; apply Rlt_Rminus; elim H5; clear H5; intros; + unfold disc in H7; apply H7. + exists (mkposreal _ H7); unfold included in |- *; intros; split. + assumption. + exists x1; split. + apply H4. + elim H5; intros; split. + assumption. + unfold disc in H8; simpl in H8; unfold disc in |- *; simpl in |- *; + unfold disc in H10; simpl in H10; + apply Rle_lt_trans with (Rabs (x2 - x0) + Rabs (x0 - x)). + replace (x2 - x) with (x2 - x0 + (x0 - x)); [ apply Rabs_triang | ring ]. + replace (x1 / 2) with (d + Rabs (x0 - x)); [ idtac | unfold d in |- *; ring ]. + do 2 rewrite <- (Rplus_comm (Rabs (x0 - x))); apply Rplus_lt_compat_l; + apply H8. + apply open_set_P6 with (fun _:R => False). + apply open_set_P4. + unfold eq_Dom in |- *; unfold included in |- *; intros; split. + intros; elim H4. + intros; unfold g in H4; elim H4; clear H4; intros H4 _; elim H3; apply H4. + elim (H0 _ H3); intros DF H4; unfold covering_finite in H4; elim H4; clear H4; + intros; unfold family_finite in H5; unfold domain_finite in H5; + unfold covering in H4; simpl in H4; simpl in H5; elim H5; + clear H5; intros l H5; unfold intersection_domain in H5; + cut + (forall x:R, + In x l -> + exists del : R, + 0 < del /\ + (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ + included (g x) (fun z:R => Rabs (z - x) < del / 2)). + intros; + assert + (H7 := + Rlist_P1 l + (fun x del:R => + 0 < del /\ + (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ + included (g x) (fun z:R => Rabs (z - x) < del / 2)) H6); + elim H7; clear H7; intros l' H7; elim H7; clear H7; + intros; set (D := MinRlist l'); cut (0 < D / 2). + intro; exists (mkposreal _ H9); intros; assert (H13 := H4 _ H10); elim H13; + clear H13; intros xi H13; assert (H14 : In xi l). + unfold g in H13; decompose [and] H13; elim (H5 xi); intros; apply H14; split; + assumption. + elim (pos_Rl_P2 l xi); intros H15 _; elim (H15 H14); intros i H16; elim H16; + intros; apply Rle_lt_trans with (Rabs (f0 x - f0 xi) + Rabs (f0 xi - f0 y)). + replace (f0 x - f0 y) with (f0 x - f0 xi + (f0 xi - f0 y)); + [ apply Rabs_triang | ring ]. + rewrite (double_var eps); apply Rplus_lt_compat. + assert (H19 := H8 i H17); elim H19; clear H19; intros; rewrite <- H18 in H20; + elim H20; clear H20; intros; apply H20; unfold included in H21; + apply Rlt_trans with (pos_Rl l' i / 2). + apply H21. + elim H13; clear H13; intros; assumption. + unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2. + prove_sup0. + rewrite Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym. + rewrite Rmult_1_r; pattern (pos_Rl l' i) at 1 in |- *; rewrite <- Rplus_0_r; + rewrite double; apply Rplus_lt_compat_l; apply H19. + discrR. + assert (H19 := H8 i H17); elim H19; clear H19; intros; rewrite <- H18 in H20; + elim H20; clear H20; intros; rewrite <- Rabs_Ropp; + rewrite Ropp_minus_distr; apply H20; unfold included in H21; + elim H13; intros; assert (H24 := H21 x H22); + apply Rle_lt_trans with (Rabs (y - x) + Rabs (x - xi)). + replace (y - xi) with (y - x + (x - xi)); [ apply Rabs_triang | ring ]. + rewrite (double_var (pos_Rl l' i)); apply Rplus_lt_compat. + apply Rlt_le_trans with (D / 2). + rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H12. + unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ 2)); + apply Rmult_le_compat_l. + left; apply Rinv_0_lt_compat; prove_sup0. + unfold D in |- *; apply MinRlist_P1; elim (pos_Rl_P2 l' (pos_Rl l' i)); + intros; apply H26; exists i; split; + [ rewrite <- H7; assumption | reflexivity ]. + assumption. + unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ unfold D in |- *; apply MinRlist_P2; intros; elim (pos_Rl_P2 l' y); intros; + elim (H10 H9); intros; elim H12; intros; rewrite H14; + rewrite <- H7 in H13; elim (H8 x H13); intros; + apply H15 + | apply Rinv_0_lt_compat; prove_sup0 ]. + intros; elim (H5 x); intros; elim (H8 H6); intros; + set + (E := + fun zeta:R => + 0 < zeta <= M - m /\ + (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)); + assert (H11 : bound E). + unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *; + unfold E in |- *; intros; elim H11; clear H11; intros H11 _; + elim H11; clear H11; intros _ H11; apply H11. + assert (H12 : exists x : R, E x). + assert (H13 := H _ H9); unfold continuity_pt in H13; + unfold continue_in in H13; unfold limit1_in in H13; + unfold limit_in in H13; simpl in H13; unfold R_dist in H13; + elim (H13 _ (H1 eps)); intros; elim H12; clear H12; + intros; exists (Rmin x0 (M - m)); unfold E in |- *; + intros; split. + split; + [ unfold Rmin in |- *; case (Rle_dec x0 (M - m)); intro; + [ apply H12 | apply Rlt_Rminus; apply Hyp ] + | apply Rmin_r ]. + intros; case (Req_dec x z); intro. + rewrite H16; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + apply (H1 eps). + apply H14; split; + [ unfold D_x, no_cond in |- *; split; [ trivial | assumption ] + | apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H15 | apply Rmin_l ] ]. + assert (H13 := completeness _ H11 H12); elim H13; clear H13; intros; + cut (0 < x0 <= M - m). + intro; elim H13; clear H13; intros; exists x0; split. + assumption. + split. + intros; cut (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp). + intros; elim H16; intros; elim H17; clear H17; intros; unfold E in H18; + elim H18; intros; apply H20; elim H17; intros; assumption. + elim (classic (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp)); intro. + assumption. + assert + (H17 := + not_ex_all_not _ (fun alp:R => Rabs (z - x) < alp <= x0 /\ E alp) H16); + unfold is_lub in p; elim p; intros; cut (is_upper_bound E (Rabs (z - x))). + intro; assert (H21 := H19 _ H20); + elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H15 H21)). + unfold is_upper_bound in |- *; intros; unfold is_upper_bound in H18; + assert (H21 := H18 _ H20); case (Rle_dec x1 (Rabs (z - x))); + intro. + assumption. + elim (H17 x1); split. + split; [ auto with real | assumption ]. + assumption. + unfold included, g in |- *; intros; elim H15; intros; elim H17; intros; + decompose [and] H18; cut (x0 = x2). + intro; rewrite H20; apply H22. + unfold E in p; eapply is_lub_u. + apply p. + apply H21. + elim H12; intros; unfold E in H13; elim H13; intros H14 _; elim H14; + intros H15 _; unfold is_lub in p; elim p; intros; + unfold is_upper_bound in H16; unfold is_upper_bound in H17; + split. + apply Rlt_le_trans with x1; [ assumption | apply (H16 _ H13) ]. + apply H17; intros; unfold E in H18; elim H18; intros; elim H19; intros; + assumption. Qed. |