proposition: Lemma open_set_P3 : forall D1 D2:R -> Prop, open_set D1 -> open_set D2 -> open_set (intersection_domain D1 D2).
proof: Proof. unfold open_set; intros; unfold intersection_domain in H1; elim H1; intros. assert (H4 := H _ H2); assert (H5 := H0 _ H3); unfold intersection_domain; unfold neighbourhood in H4, H5; elim H4; clear H; intros del1 H; elim H5; clear H0; intros del2 H0; cut (0 < Rmin del1 del2). - intro; set (del := mkposreal _ H6). exists del; unfold included; intros; unfold included in H, H0; unfold disc in H, H0, H7. split. + apply H; apply Rlt_le_trans with (pos del). * apply H7. * unfold del; simpl; apply Rmin_l. + apply H0; apply Rlt_le_trans with (pos del). * apply H7. * unfold del; simpl; apply Rmin_r. - unfold Rmin; case (Rle_dec del1 del2); intro. + apply (cond_pos del1). + apply (cond_pos del2). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type