proposition: Lemma Heine_cor1 : forall (f:R -> R) (a b:R), a < b -> (forall x:R, a <= x <= b -> continuity_pt f x) -> forall eps:posreal, { delta:posreal | delta <= b - a /\ (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; set (E := fun l:R => 0 < l <= b - a /\ (forall x y:R, a <= x <= b -> a <= y <= b -> Rabs (x - y) < l -> Rabs (f x - f y) < eps)); assert (H1 : bound E). { unfold bound; exists (b - a); unfold is_upper_bound; intros; unfold E in H1; elim H1; clear H1; intros H1 _; elim H1; intros; assumption. } assert (H2 : exists x : R, E x). { assert (H2 := Heine f (fun x:R => a <= x <= b) (compact_P3 a b) H0 eps); elim H2; intros; exists (Rmin x (b - a)); unfold E; split; [ split; [ unfold Rmin; case (Rle_dec x (b - a)); intro; [ apply (cond_pos x) | apply Rlt_0_minus; assumption ] | apply Rmin_r ] | intros; apply H3; try assumption; apply Rlt_le_trans with (Rmin x (b - a)); [ assumption | apply Rmin_l ] ]. } assert (H3 := completeness E H1 H2); elim H3; intros x p; cut (0 < x <= b - a). { intro; elim H4; clear H4; intros; exists (mkposreal _ H4); split. { apply H5. } unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6; set (D := Rabs (x0 - y)). assert (H11: ((exists y : R, D < y /\ E y) \/ (forall y : R, not (D < y /\ E y)) -> False) -> False). { clear; intros H; apply H. right; intros y0 H0; apply H. left; now exists y0. } apply Rnot_le_lt; intros H30. apply H11; clear H11; intros H11. revert H30; apply Rlt_not_le. destruct H11 as [H11|H12]. { elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13; intros; apply H15; assumption. } assert (H13 : is_upper_bound E D). { unfold is_upper_bound; intros; assert (H14 := H12 x1); apply Rnot_lt_le; contradict H14; now split. } assert (H14 := H7 _ H13); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H10)). } unfold is_lub in p; unfold is_upper_bound in p; elim p; clear p; intros; split. { elim H2; intros; assert (H7 := H4 _ H6); unfold E in H6; elim H6; clear H6; intros H6 _; elim H6; intros; apply Rlt_le_trans with x0; assumption. } apply H5; intros; unfold E in H6; elim H6; clear H6; intros H6 _; elim H6; intros; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra