diff options
Diffstat (limited to 'theories/Reals/Rtopology.v')
| -rw-r--r-- | theories/Reals/Rtopology.v | 1825 |
1 files changed, 1825 insertions, 0 deletions
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v new file mode 100644 index 00000000..1c112bf1 --- /dev/null +++ b/theories/Reals/Rtopology.v @@ -0,0 +1,1825 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Rtopology.v,v 1.19.2.1 2004/07/16 19:31:13 herbelin Exp $ i*) + +Require Import Rbase. +Require Import Rfunctions. +Require Import Ranalysis1. +Require Import RList. +Require Import Classical_Prop. +Require Import Classical_Pred_Type. Open Local Scope R_scope. + +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. +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. +Definition closed_set (D:R -> Prop) : Prop := open_set (complementary D). +Definition intersection_domain (D1 D2:R -> Prop) (c:R) : Prop := D1 c /\ D2 c. +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). +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. +Qed. + +Definition point_adherent (D:R -> Prop) (x:R) : Prop := + forall V:R -> Prop, + neighbourhood V x -> exists y : R, intersection_domain V D y. +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. +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. +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. +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. +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. +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 ]. +Qed. + +Definition eq_Dom (D1 D2:R -> Prop) : Prop := + included D1 D2 /\ included D2 D1. + +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). +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). +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)). +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. +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). +Qed. + +Lemma open_set_P4 : open_set (fun x:R => False). +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. +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. +Qed. + +Lemma continuity_P1 : + forall (f:R -> R) (x:R), + continuity_pt f x <-> + (forall W:R -> Prop, + neighbourhood W (f x) -> + 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. +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)). +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. +Qed. + +(**********) +Theorem Rsepare : + forall x y:R, + x <> y -> + exists V : 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. +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}. + +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). + +Definition family_finite (f:family) : Prop := domain_finite (ind f). + +Definition covering (D:R -> Prop) (f:family) : Prop := + forall x:R, D x -> exists y : R, f y x. + +Definition covering_open_set (D:R -> Prop) (f:family) : Prop := + covering D f /\ family_open_set f. + +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. +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). + +Definition compact (X:R -> Prop) : Prop := + forall f:family, + covering_open_set X f -> + 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. +Qed. + +Definition bounded (D:R -> Prop) : Prop := + 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. +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)) ]. +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. +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. +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. +Qed. + +(* 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. +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. +(* 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. +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). +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). +Qed. + +Definition image_dir (f:R -> R) (D:R -> Prop) (x:R) : Prop := + 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. +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 ]. +Qed. + +Lemma prolongement_C0 : + forall (f:R -> R) (a b:R), + a <= b -> + (forall c:R, a <= c <= b -> continuity_pt f c) -> + exists g : R -> R, + continuity g /\ (forall c:R, a <= c <= b -> g c = f c). +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) -> + 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 -> + 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. +Qed. + +(**********) +Lemma continuity_ab_min : + 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). +Qed. + + +(********************************************************) +(* Proof of Bolzano-Weierstrass theorem *) +(********************************************************) + +Definition ValAdh (un:nat -> R) (x:R) : Prop := + forall (V:R -> Prop) (N:nat), + neighbourhood V x -> exists p : nat, (N <= p)%nat /\ V (un p). + +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 + (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. +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 + (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x) in + 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. +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) ]. +Qed. + +Definition family_closed_set (f:family) : Prop := + forall x:R, closed_set (f x). + +Definition intersection_vide_in (D:R -> Prop) (f:family) : Prop := + forall x:R, + (ind f x -> included (f x) D) /\ + ~ (exists y : R, intersection_family f y). + +Definition intersection_vide_finite_in (D:R -> Prop) + (f:family) : Prop := intersection_vide_in D f /\ family_finite f. + +(**********) +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 -> + 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) ]. +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. +Qed. + +(********************************************************) +(* Proof of Heine's theorem *) +(********************************************************) + +Definition uniform_continuity (f:R -> R) (X:R -> Prop) : Prop := + forall eps:posreal, + exists delta : posreal, + (forall x y:R, + 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) ]. +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. +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. +(* 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. +(* 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). +(* 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 => + 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. +Qed. |