proposition: Lemma continuity_open_interval_continuity : forall f, (forall lb ub, continuity_open_interval lb ub f) -> continuity f.
proof: Proof. intros f Hf x eps eps_pos ; destruct (Hf _ _ _ (center_in_open_interval x 1 Rlt_0_1) _ eps_pos) as [delta [delta_pos Hdelta]] ; exists (Rmin delta 1) ; split. apply Rmin_pos_lt ; lra. simpl ; intros y [[_ y_neq] y_b] ; apply Hdelta ; split. rewrite <- Rball_rewrite ; 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