proposition: Lemma interior_P3 : forall D:R -> Prop, open_set (interior D).
proof: Proof. intro; unfold open_set, interior; unfold neighbourhood; intros; elim H; 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; 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; rewrite <- (Rabs_Ropp (x - x1)); rewrite Ropp_minus_distr; ring. - unfold del; apply Rplus_lt_reg_l with (Rabs (x - x1)); rewrite Rplus_0_r; replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0); [ idtac | ring ]. unfold disc in H1; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type