diff options
Diffstat (limited to 'theories/Reals/Rtopology.v')
| -rw-r--r-- | theories/Reals/Rtopology.v | 696 |
1 files changed, 347 insertions, 349 deletions
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 8e9b2bb3..51d0b99e 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -1,20 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtopology.v 14641 2011-11-06 11:59:10Z herbelin $ 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. +Local Open Scope R_scope. (** * General definitions and propositions *) @@ -32,16 +30,16 @@ 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; + intros; unfold included; unfold interior; intros; unfold neighbourhood in H; elim H; intros; unfold included in H0; - apply H0; unfold disc in |- *; unfold Rminus in |- *; + apply H0; unfold disc; unfold Rminus; 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. + intros; unfold open_set in H; unfold included; intros; + assert (H1 := H _ H0); unfold interior; apply H1. Qed. Definition point_adherent (D:R -> Prop) (x:R) : Prop := @@ -51,11 +49,11 @@ 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. + intro; unfold included; intros; unfold adherence; + unfold point_adherent; intros; exists x; + unfold intersection_domain; split. unfold neighbourhood in H0; elim H0; intros; unfold included in H1; apply H1; - unfold disc in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; + unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos x0). apply H. Qed. @@ -64,29 +62,29 @@ 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. + unfold included; 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 |- *; + intro; unfold open_set, interior; unfold neighbourhood; intros; elim H; intros. - exists x0; unfold included in |- *; intros. + exists x0; unfold included; 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. + unfold included; unfold disc; 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; + unfold del; rewrite <- (Rabs_Ropp (x - x1)); rewrite Ropp_minus_distr; ring. - unfold del in |- *; apply Rplus_lt_reg_r with (Rabs (x - x1)); + unfold del; 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 ]. @@ -97,7 +95,7 @@ Lemma complementary_P1 : forall D:R -> Prop, ~ (exists y : R, intersection_domain D (complementary D) y). Proof. - intro; red in |- *; intro; elim H; intros; + intro; red; intro; elim H; intros; unfold intersection_domain, complementary in H0; elim H0; intros; elim H2; assumption. Qed. @@ -105,8 +103,8 @@ 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)); + unfold closed_set; unfold open_set, complementary; intros; + unfold included, adherence; intros; assert (H1 := classic (D x)); elim H1; intro. assumption. assert (H3 := H _ H2); assert (H4 := H0 _ H3); elim H4; intros; @@ -116,8 +114,8 @@ 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 |- *; + intro; unfold closed_set, adherence; + unfold open_set, complementary, point_adherent; intros; set (P := @@ -125,21 +123,21 @@ Proof. 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. + unfold neighbourhood; elim H2; intros; unfold neighbourhood in H3; + elim H3; intros; exists x0; unfold included; + intros; red; 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 |- *; + unfold included in H5; apply H5; unfold disc; 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)); + unfold del; simpl; 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); @@ -154,10 +152,10 @@ 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. + intro; unfold eq_Dom; split. apply interior_P2; assumption. apply interior_P1. - intro; unfold eq_Dom in H; elim H; clear H; intros; unfold open_set in |- *; + intro; unfold eq_Dom in H; elim H; clear H; intros; unfold open_set; intros; unfold included, interior in H; unfold included in H0; apply (H _ H1). Qed. @@ -165,20 +163,20 @@ 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. + intro; unfold eq_Dom; split. apply adherence_P1. apply adherence_P2; assumption. - unfold eq_Dom in |- *; unfold included in |- *; intros; + unfold eq_Dom; unfold included; intros; assert (H0 := adherence_P3 D); unfold closed_set in H0; - unfold closed_set in |- *; unfold open_set in |- *; + unfold closed_set; unfold open_set; unfold open_set in H0; intros; assert (H2 : complementary (adherence D) x). - unfold complementary in |- *; unfold complementary in H1; red in |- *; intro; + unfold complementary; unfold complementary in H1; red; intro; elim H; clear H; intros _ H; elim H1; apply (H _ H2). - assert (H3 := H0 _ H2); unfold neighbourhood in |- *; + assert (H3 := H0 _ H2); unfold neighbourhood; unfold neighbourhood in H3; elim H3; intros; exists x0; - unfold included in |- *; unfold included in H4; intros; + unfold included; unfold included in H4; intros; assert (H6 := H4 _ H5); unfold complementary in H6; - unfold complementary in |- *; red in |- *; intro; + unfold complementary; red; intro; elim H; clear H; intros H _; elim H6; apply (H _ H7). Qed. @@ -186,8 +184,8 @@ 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; + unfold included, neighbourhood; intros; elim H0; intros; exists x0; + intros; unfold included; unfold included in H1; intros; apply (H _ (H1 _ H2)). Qed. @@ -195,12 +193,12 @@ 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. + unfold open_set; intros; unfold union_domain in H1; elim H1; intro. apply neighbourhood_P1 with D1. - unfold included, union_domain in |- *; tauto. + unfold included, union_domain; tauto. apply H; assumption. apply neighbourhood_P1 with D2. - unfold included, union_domain in |- *; tauto. + unfold included, union_domain; tauto. apply H0; assumption. Qed. @@ -208,53 +206,53 @@ 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; + unfold open_set; 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; + unfold intersection_domain; 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; + exists del; unfold included; 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. + unfold del; simpl; 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. + unfold del; simpl; apply Rmin_r. + unfold Rmin; 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. + unfold open_set; 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. + unfold open_set; intros; unfold neighbourhood. + exists (mkposreal 1 Rlt_0_1); unfold included; 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; + unfold eq_Dom; split. + unfold included, interior, disc; intros; cut (0 < del - Rabs (x - x0)). intro; set (del2 := mkposreal _ H3). - exists del2; unfold included in |- *; intros. + exists del2; unfold included; 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)); + unfold del2; simpl; 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); @@ -280,19 +278,19 @@ Proof. elim H3; intros. exists (disc x (mkposreal del2 H4)). intros; unfold included in H1; split. - unfold neighbourhood, disc in |- *. + unfold neighbourhood, disc. 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; + unfold included; intros; assumption. + intros; apply H1; unfold disc; case (Req_dec y x); intro. + rewrite H7; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos del1). apply H5; split. - unfold D_x, no_cond in |- *; split. + unfold D_x, no_cond; split. trivial. - apply (sym_not_eq (A:=R)); apply H7. + apply (not_eq_sym (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; unfold continuity_pt; unfold continue_in; + unfold limit1_in; unfold limit_in; intros. assert (H1 := H (disc (f x) (mkposreal eps H0))). cut (neighbourhood (disc (f x) (mkposreal eps H0)) (f x)). @@ -301,10 +299,10 @@ Proof. 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. + intros; elim H8; intros; simpl in H10; unfold R_dist in H10; simpl; + unfold R_dist; apply (H6 _ (H7 _ H10)). + unfold neighbourhood, disc; exists (mkposreal eps H0); + unfold included; intros; assumption. Qed. Definition image_rec (f:R -> R) (D:R -> Prop) (x:R) : Prop := D (f x). @@ -314,13 +312,13 @@ 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; + intros; unfold open_set in H0; unfold open_set; intros; assert (H2 := continuity_P1 f x); elim H2; intros H3 _; - assert (H4 := H3 (H x)); unfold neighbourhood, image_rec in |- *; + assert (H4 := H3 (H x)); unfold neighbourhood, image_rec; 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)). + unfold included; intros; apply (H8 _ (H9 _ H10)). Qed. (**********) @@ -331,9 +329,9 @@ Lemma continuity_P3 : 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; unfold continuity; unfold continuity_pt; + unfold continue_in; unfold limit1_in; + unfold limit_in; simpl; unfold R_dist; 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)). @@ -342,7 +340,7 @@ Proof. 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; + unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0. apply disc_P1. Qed. @@ -360,23 +358,23 @@ Proof. 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 |- *; + unfold neighbourhood; exists (mkposreal _ H); unfold included; tauto. split. - unfold neighbourhood in |- *; exists (mkposreal _ H); unfold included in |- *; + unfold neighbourhood; exists (mkposreal _ H); unfold included; tauto. - red in |- *; intro; elim H0; intros; unfold intersection_domain in H1; + red; 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 |- *; + change (Rabs (x - y) < D); 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). + unfold Rdiv; apply Rmult_lt_0_compat. + unfold D; apply Rabs_pos_lt; apply (Rminus_eq_contra _ _ Hsep). apply Rinv_0_lt_compat; prove_sup0. Qed. @@ -406,7 +404,7 @@ Lemma restriction_family : (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; + intros; elim H; intros; unfold intersection_domain; elim H0; intros; split. apply (cond_fam f0); exists x0; assumption. assumption. @@ -426,19 +424,19 @@ 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)). + unfold family_open_set; intros; unfold subfamily; + simpl; 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; + unfold open_set; unfold neighbourhood; intros; elim H3; intros; assert (H6 := H2 _ H4); elim H6; intros; exists x1; - unfold included in |- *; intros; split. + unfold included; 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; + unfold open_set; unfold neighbourhood; intros; elim H3; intros; elim H1; assumption. Qed. @@ -448,7 +446,7 @@ Definition bounded (D:R -> Prop) : Prop := 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 open_set; unfold neighbourhood; intros. unfold eq_Dom in H0; elim H0; intros. assert (H4 := H _ (H3 _ H1)). elim H4; intros. @@ -467,7 +465,7 @@ Proof. 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). + unfold bounded; 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; @@ -486,25 +484,25 @@ Proof. 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; + unfold intersection_domain, D; tauto. + unfold covering_open_set; split. + unfold covering; intros; simpl; exists (Rabs x + 1); + unfold g; pattern (Rabs x) at 1; 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. + unfold family_open_set; 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; + unfold eq_Dom; unfold f0; simpl; + unfold g, disc; split. + unfold included; 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; + unfold included; intros; unfold Rminus; 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; + unfold eq_Dom; split. + unfold included; intros; elim H3. + unfold included, f0; simpl; unfold g; intros; elim H2; intro; [ rewrite <- H4 in H3; assert (H5 := Rabs_pos x0); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H3)) @@ -517,10 +515,10 @@ 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. + unfold eq_Dom; split. apply adherence_P1. - unfold included in |- *; unfold adherence in |- *; - unfold point_adherent in |- *; intros; unfold compact in H; + unfold included; unfold adherence; + unfold point_adherent; 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). @@ -550,44 +548,44 @@ Proof. 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 |- *; + elim (H8 y0); clear H8; intros; apply H8; unfold intersection_domain; 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; + unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply H9. - unfold alp in |- *; apply MinRlist_P2; intros; + unfold alp; 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 |- *; + unfold covering_open_set; split. + unfold covering; intros; exists x0; simpl; unfold g; split. - unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + unfold Rminus; 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 |- *; + unfold family_open_set; intro; simpl; unfold g; 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. + unfold eq_Dom; split. + unfold included, disc; simpl; 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; + unfold included, disc; simpl; 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. + unfold eq_Dom; split. + unfold included; intros; elim H6. + unfold included; 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; + intros; unfold Rdiv; apply Rmult_lt_0_compat. + apply Rabs_pos_lt; apply Rminus_eq_contra; red; intro; rewrite H3 in H2; elim H1; apply H2. apply Rinv_0_lt_compat; prove_sup0. Qed. @@ -595,29 +593,29 @@ 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. + unfold compact; intros; exists (fun x:R => False); + unfold covering_finite; split. + unfold covering; intros; elim H0. + unfold family_finite; unfold domain_finite; exists nil; intro. split. - simpl in |- *; unfold intersection_domain in |- *; intros; elim H0. + simpl; unfold intersection_domain; intros; elim H0. elim H0; clear H0; intros _ H0; elim H0. - simpl in |- *; intro; elim H0. + simpl; 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; + unfold compact; intros; unfold eq_Dom in H0; elim H0; clear H0; + unfold included; intros; assert (H3 : covering_open_set X1 f0). + unfold covering_open_set; unfold covering_open_set in H1; elim H1; clear H1; intros; split. - unfold covering in H1; unfold covering in |- *; intros; + unfold covering in H1; unfold covering; intros; apply (H1 _ (H0 _ H4)). apply H3. - elim (H _ H3); intros D H4; exists D; unfold covering_finite in |- *; + elim (H _ H3); intros D H4; exists D; unfold covering_finite; unfold covering_finite in H4; elim H4; intros; split. - unfold covering in H5; unfold covering in |- *; intros; + unfold covering in H5; unfold covering; intros; apply (H5 _ (H2 _ H7)). apply H6. Qed. @@ -626,7 +624,7 @@ Qed. 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; + unfold compact; intros; set (A := fun x:R => @@ -649,92 +647,92 @@ Proof. 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; + unfold covering_finite; split. + unfold covering; 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; + simpl in H16; simpl; unfold Db; 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; + exists y0; simpl; split. + apply H8; unfold disc; 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; + unfold Rminus; 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 Db; right; reflexivity. + unfold family_finite; unfold domain_finite; 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; + simpl; left; apply H16. + simpl; right; apply H13. + simpl; unfold intersection_domain; 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 |- *. + intro; simpl in H14; elim H14; intro; simpl; + unfold intersection_domain. 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). + unfold Db; right; assumption. + simpl; unfold intersection_domain; 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. + unfold Db; 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; + unfold m'; unfold Rmin; case (Rle_dec (m + eps / 2) b); intro. + pattern m at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; + unfold Rdiv; 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. + unfold A; 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; + unfold m'; unfold Rmin; case (Rle_dec (m + eps / 2) b); intro. + pattern m at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; + unfold Rdiv; 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 m'; 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; + unfold covering_finite; split. + unfold covering; 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 |- *. + simpl in H16; simpl; unfold Db. 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)); + exists y0; simpl; split. + apply H8; unfold disc; unfold Rabs; 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; + unfold Rminus; 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). @@ -743,56 +741,56 @@ Proof. ring. ring. apply Rle_lt_trans with (m' - m). - unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (- m)); + unfold Rminus; 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. + unfold m'; 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; + unfold Rdiv; 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 Rmult_1_l; pattern (pos eps) at 1; 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 Db; right; reflexivity. + unfold family_finite; unfold domain_finite; 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; + simpl; left; apply H16. + simpl; right; apply H13; simpl; + unfold intersection_domain; 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 |- *. + intro; simpl in H14; elim H14; intro; simpl; + unfold intersection_domain. split. apply (cond_fam f0); rewrite H15; exists m; apply H6. - unfold Db in |- *; right; assumption. + unfold Db; 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. + unfold Db; 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 |- *; + pattern m at 2; rewrite <- Rplus_0_r; unfold Rminus; 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; + unfold is_upper_bound; intros; assert (H14 := not_and_or _ _ (H12 x)); elim H14; intro. elim H15; apply H13. @@ -805,44 +803,44 @@ Proof. 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; + apply (H4 b); unfold is_upper_bound; 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 bound; exists b; unfold is_upper_bound; intros; unfold A in H1; elim H1; clear H1; intros H1 _; elim H1; clear H1; intros _ H1; apply H1. - unfold A in |- *; split. + unfold A; 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). + unfold covering_finite; split. + unfold covering; simpl; intros; cut (x = a). intro; exists y0; split. rewrite H4; apply H2. - unfold D' in |- *; reflexivity. + unfold D'; reflexivity. elim H3; intros; apply Rle_antisym; assumption. - unfold family_finite in |- *; unfold domain_finite in |- *; + unfold family_finite; unfold domain_finite; exists (cons y0 nil); intro; split. - simpl in |- *; unfold intersection_domain in |- *; intro; elim H3; clear H3; + simpl; unfold intersection_domain; intro; elim H3; clear H3; intros; unfold D' in H4; left; apply H4. - simpl in |- *; unfold intersection_domain in |- *; intro; elim H3; intro. + simpl; unfold intersection_domain; 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; + unfold eq_Dom; split. + unfold included; intros; elim H. + unfold included; 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)); + unfold compact; 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). @@ -850,61 +848,61 @@ Proof. 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; + unfold covering_finite; 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 |- *; + unfold covering; unfold covering in H5; intros. + elim (H5 _ (H1 _ H7)); intros y0 H8; exists y0; simpl in H8; simpl; 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; unfold domain_finite; 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 |- *; + intro; apply H7; simpl; unfold intersection_domain; + simpl in H9; unfold intersection_domain in H9; unfold D'; apply H9. intro; assert (H10 := H8 H9); simpl in H10; unfold intersection_domain in H10; - simpl in |- *; unfold intersection_domain in |- *; + simpl; unfold intersection_domain; unfold D' in H10; apply H10. - unfold covering_open_set in |- *; unfold covering_open_set in H2; elim H2; + unfold covering_open_set; unfold covering_open_set in H2; elim H2; clear H2; intros. split. - unfold covering in |- *; unfold covering in H2; intros. + unfold covering; unfold covering in H2; intros. elim (classic (F x)); intro. - elim (H2 _ H6); intros y0 H7; exists y0; simpl in |- *; unfold g' in |- *; + elim (H2 _ H6); intros y0 H7; exists y0; simpl; unfold g'; left; assumption. cut (exists z : R, D z). - intro; elim H7; clear H7; intros x0 H7; exists x0; simpl in |- *; - unfold g' in |- *; right. + intro; elim H7; clear H7; intros x0 H7; exists x0; simpl; + unfold g'; right. split. - unfold complementary in |- *; apply H6. + unfold complementary; 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 |- *; + unfold family_open_set; intro; simpl; unfold g'; 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. + unfold eq_Dom; split. + unfold included, union_domain, complementary; intros. elim H6; intro; [ left; apply H7 | right; split; assumption ]. - unfold included, union_domain, complementary in |- *; intros. + unfold included, union_domain, complementary; 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. + unfold eq_Dom; split. + unfold included, complementary; intros; left; apply H6. + unfold included, complementary; intros. elim H6; intro. apply H7. elim H7; intros _ H8; elim H5; apply H8. @@ -916,9 +914,9 @@ Proof. 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; + unfold eq_Dom; split. + unfold included; intros; elim H3. + assert (H3 := not_ex_all_not _ _ Hyp_F_NE); unfold included; intros; elim (H3 x); apply H4. Qed. @@ -949,7 +947,7 @@ 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. + unfold compact; 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). @@ -958,24 +956,24 @@ Proof. 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; + unfold covering_finite; split. + unfold covering, image_dir; simpl; 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 |- *; + unfold family_finite; unfold domain_finite; elim H6; intros l H7; exists l; intro; elim (H7 x); intros; split; intro. - apply H8; simpl in H10; simpl in |- *; apply H10. + apply H8; simpl in H10; simpl; 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 |- *; + unfold covering_open_set; split. + unfold covering; intros; simpl; unfold covering in H1; + unfold image_dir in H1; unfold g; unfold image_rec; 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 |- *; + unfold family_open_set; unfold family_open_set in H2; intro; + simpl; unfold g; 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)). @@ -1012,16 +1010,16 @@ Proof. 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); + unfold continuity; intro; case (Rtotal_order x a); intro. + unfold continuity_pt; unfold continue_in; + unfold limit1_in; unfold limit_in; + simpl; unfold R_dist; intros; exists (a - x); split. - change (0 < a - x) in |- *; apply Rlt_Rminus; assumption. - intros; elim H5; clear H5; intros _ H5; unfold h in |- *. + change (0 < a - x); apply Rlt_Rminus; assumption. + intros; elim H5; clear H5; intros _ H5; unfold h. case (Rle_dec x a); intro. case (Rle_dec x0 a); intro. - unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + unfold Rminus; 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. @@ -1032,23 +1030,23 @@ Proof. 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 |- *; + unfold R_dist in H6; unfold continuity_pt; + unfold continue_in; unfold limit1_in; + unfold limit_in; simpl; unfold R_dist; intros; elim (H6 _ H7); intros; exists (Rmin x0 (b - a)); split. - unfold Rmin in |- *; case (Rle_dec x0 (b - a)); intro. + unfold Rmin; case (Rle_dec x0 (b - a)); intro. elim H8; intros; assumption. - change (0 < b - a) in |- *; apply Rlt_Rminus; assumption. + change (0 < b - a); apply Rlt_Rminus; assumption. intros; elim H9; clear H9; intros _ H9; cut (x1 < b). - intro; unfold h in |- *; case (Rle_dec x a); intro. + intro; unfold h; case (Rle_dec x a); intro. case (Rle_dec x1 a); intro. - unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + unfold Rminus; 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. + unfold D_x, no_cond; split. trivial. - red in |- *; intro; elim n; right; symmetry in |- *; assumption. + red; intro; elim n; right; symmetry ; assumption. apply Rlt_le_trans with (Rmin x0 (b - a)). rewrite H4 in H9; apply H9. apply Rmin_l. @@ -1065,9 +1063,9 @@ Proof. 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 |- *; + unfold R_dist in H7; unfold continuity_pt; + unfold continue_in; unfold limit1_in; + unfold limit_in; simpl; unfold R_dist; intros; elim (H7 _ H8); intros; elim H9; clear H9; intros. assert (H11 : 0 < x - a). @@ -1075,7 +1073,7 @@ Proof. 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. + unfold Rmin; case (Rle_dec (x - a) (b - x)); intro. case (Rle_dec x0 (x - a)); intro. assumption. assumption. @@ -1083,7 +1081,7 @@ Proof. 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 H15; clear H15; intros; unfold h; case (Rle_dec x a); intro. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). case (Rle_dec x b); intro. @@ -1117,16 +1115,16 @@ Proof. 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 |- *; + unfold R_dist in H8; unfold continuity_pt; + unfold continue_in; unfold limit1_in; + unfold limit_in; simpl; unfold R_dist; intros; elim (H8 _ H9); intros; exists (Rmin x0 (b - a)); split. - unfold Rmin in |- *; case (Rle_dec x0 (b - a)); intro. + unfold Rmin; case (Rle_dec x0 (b - a)); intro. elim H10; intros; assumption. - change (0 < b - a) in |- *; apply Rlt_Rminus; assumption. + change (0 < b - a); apply Rlt_Rminus; assumption. intros; elim H11; clear H11; intros _ H11; cut (a < x1). - intro; unfold h in |- *; case (Rle_dec x a); intro. + intro; unfold h; 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)). @@ -1134,15 +1132,15 @@ Proof. case (Rle_dec x1 b); intro. rewrite H6; elim H10; intros; elim r0; intro. apply H14; split. - unfold D_x, no_cond in |- *; split. + unfold D_x, no_cond; split. trivial. - red in |- *; intro; rewrite <- H16 in H15; elim (Rlt_irrefl _ H15). + red; intro; rewrite <- H16 in H15; elim (Rlt_irrefl _ H15). rewrite H6 in H11; apply Rlt_le_trans with (Rmin x0 (b - a)). apply H11. apply Rmin_l. - rewrite H15; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + rewrite H15; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. - rewrite H6; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; + rewrite H6; unfold Rminus; 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; @@ -1151,18 +1149,18 @@ Proof. 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); + unfold continuity_pt; unfold continue_in; + unfold limit1_in; unfold limit_in; + simpl; unfold R_dist; intros; exists (x - b); split. - change (0 < x - b) in |- *; apply Rlt_Rminus; assumption. + change (0 < x - b); 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. + unfold h; 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)). @@ -1170,8 +1168,8 @@ Proof. 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. + unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + intros; elim H3; intros; unfold h; case (Rle_dec c a); intro. elim r; intro. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 H6)). rewrite H6; reflexivity. @@ -1212,7 +1210,7 @@ Proof. 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 ]. + unfold image_dir; exists c; split; [ reflexivity | apply H10 ]. apply H9. elim (classic (image_dir g (fun c:R => a <= c <= b) M)); intro. assumption. @@ -1227,13 +1225,13 @@ Proof. 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 |- *; + pattern M at 2; rewrite <- Rplus_0_r; unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_0; rewrite Ropp_involutive; apply (cond_pos eps). - unfold is_upper_bound, image_dir in |- *; intros; cut (x <= M). + unfold is_upper_bound, image_dir; 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. + elim (H9 x); unfold intersection_domain, disc, image_dir; 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). @@ -1251,8 +1249,8 @@ Proof. ~ 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; + red; intro; elim (H11 y). + unfold intersection_domain; unfold intersection_domain in H13; elim H13; clear H13; intros; split. apply (H12 _ H13). apply H14. @@ -1270,18 +1268,18 @@ Proof. split. apply H12. apply (not_ex_all_not _ _ H13). - red in |- *; intro; cut (adherence (image_dir g (fun c:R => a <= c <= b)) M). + red; intro; cut (adherence (image_dir g (fun c:R => a <= c <= b)) M). intro; elim (closed_set_P1 (image_dir g (fun c:R => a <= c <= b))); intros H11 _; assert (H12 := H11 H3). elim H8. unfold eq_Dom in H12; elim H12; clear H12; intros. apply (H13 _ H10). apply H9. - exists (g a); unfold image_dir in |- *; exists a; split. + exists (g a); unfold image_dir; 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 |- *; + unfold bound; unfold bounded in H4; elim H4; clear H4; intros m H4; + elim H4; clear H4; intros M H4; exists M; unfold is_upper_bound; intros; elim (H4 _ H5); intros _ H6; apply H6. apply prolongement_C0; assumption. Qed. @@ -1329,8 +1327,8 @@ 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. + unfold neighbourhood, disc; exists (mkposreal _ Rlt_0_1); + unfold included; trivial. elim (H0 _ H1); intros; unfold intersection_domain in H2; elim H2; intros; elim H4; intros; apply H6. Qed. @@ -1347,17 +1345,17 @@ 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 |- *; + unfold ValAdh in H; unfold ValAdh_un; + unfold intersection_family; simpl; + intros; elim H0; intros N H1; unfold adherence; + unfold point_adherent; intros; elim (H V N H2); + intros; exists (un x0); unfold intersection_domain; 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 ValAdh; intros; unfold ValAdh_un in H; unfold intersection_family in H; simpl in H; assert (H1 : @@ -1378,8 +1376,8 @@ 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 |- *; + unfold adherence, included; unfold point_adherent; intros; + elim (H0 _ H1); unfold intersection_domain; intros; elim H2; clear H2; intros; exists x0; split; [ assumption | apply (H _ H3) ]. Qed. @@ -1412,36 +1410,36 @@ Proof. 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; + unfold covering_open_set; split. + unfold covering; 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 |- *; + intros; unfold f0; simpl; unfold f'; split; [ apply H10 | apply H9 ]. - unfold family_open_set in |- *; intro; elim (classic (D' x)); intro. + unfold family_open_set; 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 |- *; + unfold f0; simpl; unfold f'; unfold eq_Dom; split. - unfold included in |- *; intros; split; [ apply H4 | apply H3 ]. - unfold included in |- *; intros; elim H4; intros; assumption. + unfold included; intros; split; [ apply H4 | apply H3 ]. + unfold included; 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; + unfold eq_Dom; unfold included; 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; + unfold intersection_vide_finite_in; split. + unfold intersection_vide_in; simpl; intros; split. + intros; unfold included; 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; + red; 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 _; @@ -1464,16 +1462,16 @@ Proof. 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. + intros; unfold intersection_domain; 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 |- *; + unfold family_finite; unfold domain_finite; 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) ]. + [ apply H6; simpl; simpl in H8; apply H8 | apply (H7 H8) ]. Qed. Theorem Bolzano_Weierstrass : @@ -1494,8 +1492,8 @@ Proof. 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. + unfold neighbourhood; exists (mkposreal _ Rlt_0_1); + unfold included; trivial. elim (H3 _ H4); intros; unfold intersection_domain in H5; decompose [and] H5; assumption. set (f0 := mkfamily D g H2). @@ -1511,19 +1509,19 @@ Proof. 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. + unfold intersection_family; simpl; + unfold intersection_domain; intros; split. + unfold g; 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 ]. + | rewrite <- H12; unfold r; apply MaxRlist_P1; elim (H9 y); intros; + apply H14; simpl; 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; + unfold r; 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. @@ -1543,16 +1541,16 @@ Proof. 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 |- *; + unfold intersection_vide_in; intros; split. + intro; simpl in H6; unfold f0; simpl; unfold g; apply included_trans with (adherence X). apply adherence_P4. - unfold included in |- *; intros; elim H7; intros; elim H8; intros; elim H10; + unfold included; 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. + unfold family_closed_set; unfold f0; simpl; + unfold g; intro; apply adherence_P3. Qed. (********************************************************) @@ -1568,7 +1566,7 @@ Definition uniform_continuity (f:R -> R) (X:R -> Prop) : Prop := 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; + unfold is_lub; intros; elim H; elim H0; intros; apply Rle_antisym; [ apply (H4 _ H1) | apply (H2 _ H3) ]. Qed. @@ -1583,7 +1581,7 @@ Proof. right; elim H1; intros; elim H2; intros; exists x; exists x0; intros. split; [ assumption - | split; [ assumption | apply (sym_not_eq (A:=R)); assumption ] ]. + | split; [ assumption | apply (not_eq_sym (A:=R)); assumption ] ]. left; exists x; split. assumption. intros; case (Req_dec x0 x); intro. @@ -1599,14 +1597,14 @@ Theorem Heine : Proof. intros f0 X H0 H; elim (domain_P1 X); intro Hyp. (* X is empty *) - unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); + unfold uniform_continuity; intros; exists (mkposreal _ Rlt_0_1); intros; elim Hyp; exists x; assumption. elim Hyp; clear Hyp; intro Hyp. (* X has only one element *) - unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); + unfold uniform_continuity; 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 H6; rewrite H7; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos eps). (* X has at least two distinct elements *) assert @@ -1626,9 +1624,9 @@ Proof. 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; + unfold uniform_continuity; intro; assert (H1 : forall t:posreal, 0 < t / 2). - intro; unfold Rdiv in |- *; apply Rmult_lt_0_compat; + intro; unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos t) | apply Rinv_0_lt_compat; prove_sup0 ]. set (g := @@ -1646,8 +1644,8 @@ Proof. 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 |- *; + unfold covering_open_set; split. + unfold covering; intros; exists x; simpl; unfold g; split. assumption. assert (H4 := H _ H3); unfold continuity_pt in H4; unfold continue_in in H4; @@ -1660,22 +1658,22 @@ Proof. 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 _; + unfold bound; exists (M - m); unfold is_upper_bound; + unfold E; 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; + elim H5; clear H5; intros; exists (Rmin x0 (M - m)); unfold E; intros; split. split. - unfold Rmin in |- *; case (Rle_dec x0 (M - m)); intro. + unfold Rmin; 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; + rewrite H9; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (H1 eps). apply H7; split. - unfold D_x, no_cond in |- *; split; [ trivial | assumption ]. + unfold D_x, no_cond; 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). @@ -1692,15 +1690,15 @@ Proof. 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; + unfold is_upper_bound; 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 |- *; + unfold disc; unfold Rminus; rewrite Rplus_opp_r; + rewrite Rabs_R0; simpl; unfold Rdiv; 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; @@ -1708,13 +1706,13 @@ Proof. 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)); + unfold family_open_set; intro; simpl; elim (classic (X x)); intro. - unfold g in |- *; unfold open_set in |- *; intros; elim H4; clear H4; + unfold g; unfold open_set; 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); + intros; unfold neighbourhood; case (Req_dec x x0); intro. - exists (mkposreal _ (H1 x1)); rewrite <- H6; unfold included in |- *; intros; + exists (mkposreal _ (H1 x1)); rewrite <- H6; unfold included; intros; split. assumption. exists x1; split. @@ -1723,24 +1721,24 @@ Proof. 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 d; apply Rlt_Rminus; elim H5; clear H5; intros; unfold disc in H7; apply H7. - exists (mkposreal _ H7); unfold included in |- *; intros; split. + exists (mkposreal _ H7); unfold included; 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 H8; simpl in H8; unfold disc; simpl; 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 ]. + replace (x1 / 2) with (d + Rabs (x0 - x)); [ idtac | unfold d; 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. + unfold eq_Dom; unfold included; 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; @@ -1778,10 +1776,10 @@ Proof. 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. + unfold Rdiv; 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 Rmult_1_r; pattern (pos_Rl l' i) at 1; 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; @@ -1793,15 +1791,15 @@ Proof. 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)); + unfold Rdiv; 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)); + unfold D; 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; + unfold Rdiv; apply Rmult_lt_0_compat; + [ unfold D; 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 @@ -1813,25 +1811,25 @@ Proof. 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 _; + unfold bound; exists (M - m); unfold is_upper_bound; + unfold E; 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; exists (Rmin x0 (M - m)); unfold E; intros; split. split; - [ unfold Rmin in |- *; case (Rle_dec x0 (M - m)); intro; + [ unfold Rmin; 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; + rewrite H16; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (H1 eps). apply H14; split; - [ unfold D_x, no_cond in |- *; split; [ trivial | assumption ] + [ unfold D_x, no_cond; 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). @@ -1849,14 +1847,14 @@ Proof. 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; + unfold is_upper_bound; 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; + unfold included, g; 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. |