proposition: Lemma compact_P2 : forall X:R -> Prop, compact X -> closed_set X.
proof: Proof. intros; assert (H0 := closed_set_P1 X); elim H0; clear H0; intros _ H0; apply H0; clear H0. unfold eq_Dom; split. { apply adherence_P1. } 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). 1: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). 1:intro; set (f0 := mkfamily D g H3); assert (H4 := H f0); cut (covering_open_set X f0). 1:intro; assert (H6 := H4 H5); elim H6; clear H6; intros D' H6. 1: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). 1:intro; assert (H10 := H0 (disc x (mkposreal _ H9))); cut (neighbourhood (disc x (mkposreal alp H9)) x). 1: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). 1: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 <-(Rplus_half_diag (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; split; assumption. - assert (H11 := disc_P1 x (mkposreal alp H9)); unfold open_set in H11; apply H11. unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply H9. - 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; split. + unfold covering; intros; exists x0; simpl; unfold g; split. * unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; unfold Rminus in H2; apply (H2 _ H5). * apply H5. + 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; split. ++ unfold included, disc; simpl; intros; split. ** rewrite <- (Rabs_Ropp (x0 - x1)); rewrite Ropp_minus_distr; apply H6. ** apply H5. ++ 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; 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; 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.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type