proposition: 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: 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; 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). assert (H3 := compact_P6 X H H1 f0). elim (classic (exists l : R, ValAdh_un un l)); intro. + assumption. + cut (family_closed_set f0). 1: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; simpl; unfold intersection_domain; intros; split. ++ unfold g; apply adherence_P1; split. ** exists x; split; [ reflexivity | 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; 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; intros; split. -- intro; simpl in H6; unfold f0; simpl; unfold g; apply included_trans with (adherence X). ++ apply adherence_P4. 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; unfold f0; simpl; unfold g; intro; apply adherence_P3. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type