proposition: Lemma adherence_P3 : forall D:R -> Prop, closed_set (adherence D).
proof: Proof. intro; unfold closed_set, adherence; unfold open_set, complementary, point_adherent; 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; 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; 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; simpl; rewrite <- (Rabs_Ropp (x - x1)); rewrite Ropp_minus_distr; ring. + apply Rplus_lt_reg_l 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.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type