proposition: Lemma continuity_interval_continuity_pt: forall f lb ub x, lb < ub -> continuity_interval lb ub f -> open_interval lb ub x -> continuity_pt f x.
proof: Proof. intros f lb ub x lb_lt_ub Hf x_in eps eps_pos ; assert (x_in' := open_interval_interval _ _ _ x_in) ; destruct (Hf _ x_in' _ eps_pos) as [alpha [alpha_pos Halpha]]. exists (Rmin alpha (interval_dist lb ub x)) ; split. apply Rmin_pos_lt, open_interval_dist_pos ; assumption. intros y [[_ x_neq_y] y_bd] ; apply Halpha ; split. replace y with (x + (y -x)) by ring ; apply interval_dist_bound. assumption. left ; eapply Rlt_le_trans ; [eassumption | apply Rmin_r]. eapply Rlt_le_trans ; [eassumption | apply Rmin_l]. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics