proposition: Lemma unifcont_1d (f : R -> V) a b : (forall x, a <= x <= b -> continuous f x) -> forall eps : posreal, {delta : posreal | forall x y, a <= x <= b -> a <= y <= b -> ball x delta y -> ~~ ball (f x) eps (f y)}.
proof: Proof. intros Cf eps. wlog: f Cf / (forall z : R, continuous f z) => [ Hw | {} Cf ]. destruct (C0_extension_le f a b) as [g [Cg Hg]]. by apply Cf. destruct (Hw g) as [d Hd]. intros x Hx ; apply Cg. apply Cg. exists d => x y Hx Hy Hxy. rewrite -!Hg //. by apply Hd. assert (forall (x : R), {delta : posreal | forall y : R, ball x delta y -> ~~ ball (f x) (pos_div_2 eps) (f y)}). move: (pos_div_2 eps) => {} eps x. assert (Rbar_lt 0 (Lub.Lub_Rbar (fun d => forall y : R, ball x d y -> ball (f x) eps (f y)))). case: (Lub.Lub_Rbar_correct (fun d => forall y : R, ball x d y -> ball (f x) eps (f y))). move: (Lub.Lub_Rbar _) => l H1 H2. case: (proj1 (filterlim_locally _ _) (Cf x) eps) => d Hd. eapply Rbar_lt_le_trans, H1. by apply d. by apply Hd. assert (0 < Rbar_min 1 (Lub.Lub_Rbar (fun d => forall y : R, ball x d y -> ball (f x) eps (f y)))). move: H ; case: (Lub.Lub_Rbar (fun d => forall y : R, ball x d y -> ball (f x) eps (f y))) => [l | | ] //= H0. apply Rmin_case => //. by apply Rlt_0_1. by apply Rlt_0_1. set d := mkposreal _ H0. exists d. unfold d ; clear d ; simpl. case: (Lub.Lub_Rbar_correct (fun d => forall y : R, ball x d y -> ball (f x) eps (f y))). move: (Lub.Lub_Rbar (fun d => forall y : R, ball x d y -> ball (f x) eps (f y))) H => {H0} l H0 H1 H2 y Hy. contradict Hy. apply Rle_not_lt. apply (Rbar_le_trans (Finite _) l (Finite _)). case: (l) H0 => [r | | ] //= H0. apply Rmin_r. apply H2 => d /= Hd. apply Rnot_lt_le ; contradict Hy. by apply Hd. destruct (compactness_value_1d a b (fun x => pos_div_2 (proj1_sig (H x)))) as [d Hd]. exists d => x y Hx Hy Hxy Hf. apply (Hd x Hx). case => {Hd} t [Ht]. case: H => /= delta Hdelta [Htx Hdt]. apply (Hdelta x). eapply ball_le, Htx. rewrite {2}(double_var delta). apply Rminus_le_0 ; ring_simplify. apply Rlt_le, is_pos_div_2. intro Hftx. apply (Hdelta y). rewrite (double_var delta). apply ball_triangle with x. apply Htx. by eapply ball_le, Hxy. contradict Hf. rewrite (double_var eps). eapply ball_triangle, Hf. by apply ball_sym. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq