proposition: Lemma continuity_P1 : forall (f:R -> R) (x:R), continuity_pt f x <-> (forall W:R -> Prop, neighbourhood W (f x) -> exists V : R -> Prop, neighbourhood V x /\ (forall y:R, V y -> W (f y))).
proof: Proof. intros; split. - intros; unfold neighbourhood in H0. elim H0; intros del1 H1. unfold continuity_pt in H; unfold continue_in in H; unfold limit1_in in H; unfold limit_in in H; simpl in H; unfold Rdist in H. assert (H2 := H del1 (cond_pos del1)). elim H2; intros del2 H3. elim H3; intros. exists (disc x (mkposreal del2 H4)). intros; unfold included in H1; split. + unfold neighbourhood, disc. exists (mkposreal del2 H4). unfold included; intros; assumption. + intros; apply H1; unfold disc; case (Req_dec y x); intro. * rewrite H7; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos del1). * apply H5; split. -- unfold D_x, no_cond; split. ++ trivial. ++ apply (not_eq_sym (A:=R)); apply H7. -- unfold disc in H6; apply H6. - intros; unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; intros. assert (H1 := H (disc (f x) (mkposreal eps H0))). cut (neighbourhood (disc (f x) (mkposreal eps H0)) (f x)). + intro; assert (H3 := H1 H2). elim H3; intros D H4; elim H4; intros; unfold neighbourhood in H5; elim H5; intros del1 H7. exists (pos del1); split. * apply (cond_pos del1). * intros; elim H8; intros; simpl in H10; unfold Rdist in H10; simpl; unfold Rdist; apply (H6 _ (H7 _ H10)). + unfold neighbourhood, disc; exists (mkposreal eps H0); unfold included; intros; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type