proposition: Lemma continuity_P3 : forall f:R -> R, continuity f <-> (forall D:R -> Prop, open_set D -> open_set (image_rec f D)).
proof: Proof. intros; split. - intros; apply continuity_P2; assumption. - intros; unfold continuity; unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; cut (open_set (disc (f x) (mkposreal _ H0))). + intro; assert (H2 := H _ H1). unfold open_set, image_rec in H2; cut (disc (f x) (mkposreal _ H0) (f x)). * intro; assert (H4 := H2 _ H3). unfold neighbourhood in H4; elim H4; intros del H5. exists (pos del); split. -- apply (cond_pos del). -- intros; unfold included in H5; apply H5; elim H6; intros; apply H8. * unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0. + apply disc_P1. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type