# Library Coq.Reals.Rtopology

``` 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. ```

# 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. 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. 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). 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 :=   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). 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. Proof.   unfold included in |- *; intros; apply H0; apply H; apply H1. Qed. Lemma interior_P3 : forall D:R -> Prop, open_set (interior D). 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). 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. 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). 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 :=   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. 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. 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. 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). 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). 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). Proof.   unfold open_set in |- *; intros; elim H. Qed. Lemma open_set_P5 : open_set (fun x:R => True). 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). 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,       neighbourhood W (f x) ->       exists V : R -> Prop,         neighbourhood V x /\ (forall y:R, V y -> W (f y))). 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). 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)). 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 ->     exists V : R -> Prop,       (exists W : R -> Prop,         neighbourhood V x /\         neighbourhood W y /\ ~ (exists y : R, intersection_domain V W y)). 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}. 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. 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). 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). 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)). Lemma open_set_P6 :   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. 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. 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). 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. 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
``` Lemma compact_P3 : forall a b:R, compact (fun c:R => a <= c <= b). 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. 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.   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. 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. 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. Lemma continuity_compact :   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. 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) ->     exists g : R -> R,       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) ->     exists Mx : R, (forall c:R, a <= c <= b -> f c <= f Mx) /\ a <= Mx <= b. 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. 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. 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

``` 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. 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         (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. 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). 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 :=   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). 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. 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

``` 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. 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)). 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. Proof.   intros f0 X H0 H; elim (domain_P1 X); intro Hyp.   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; 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).   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. ```