proposition: Lemma compact_P1 : forall X:R -> Prop, compact X -> bounded X.
proof: 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; 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; 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; intro; case (Rtotal_order 0 x); intro. * apply open_set_P6 with (disc 0 (mkposreal _ H2)). -- apply disc_P1. -- 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; 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; 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)) | assert (H6 := Rabs_pos x0); assert (H7 := Rlt_trans _ _ _ H3 H4); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7)) ]. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type