proposition: Lemma continuity_pt_continuity_pt_in: forall f (D : R -> Prop) x, continuity_pt f x -> continuity_pt_in D f x.
proof: Proof. intros f D x Hf Dx eps eps_pos ; destruct (Hf _ eps_pos) as [alp [alp_pos Halp]] ; exists alp ; split ; [assumption | intros y [Dy y_bd]]. destruct (Req_dec x y) as [Heq | Hneq]. subst ; rewrite R_dist_eq ; assumption. apply Halp ; repeat split ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics