proposition: Lemma Heine_cor2 : forall (f:R -> R) (a b:R), (forall x:R, a <= x <= b -> continuity_pt f x) -> forall eps:posreal, { delta:posreal | forall x y:R, a <= x <= b -> a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps }.
proof: Proof. intro f; intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. - assert (H0 := Heine_cor1 Hlt H eps); elim H0; intros x p; exists x; elim p; intros; apply H2; assumption. - exists (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y); [ elim H0; elim H1; intros; rewrite Heq in H3, H5; apply Rle_antisym; apply Rle_trans with b; assumption | rewrite H3; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos eps) ]. - exists (mkposreal _ Rlt_0_1); intros; elim H0; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H3 H4) Hgt)). Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra