proposition: Lemma continuity_P2 : forall (f:R -> R) (D:R -> Prop), continuity f -> open_set D -> open_set (image_rec f D).
proof: Proof. intros; unfold open_set in H0; unfold open_set; intros; assert (H2 := continuity_P1 f x); elim H2; intros H3 _; assert (H4 := H3 (H x)); unfold neighbourhood, image_rec; unfold image_rec in H1; assert (H5 := H4 D (H0 (f x) H1)); elim H5; intros V0 H6; elim H6; intros; unfold neighbourhood in H7; elim H7; intros del H9; exists del; unfold included in H9; unfold included; intros; apply (H8 _ (H9 _ H10)). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type