proposition: Lemma unifcont_normed_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_norm (f x) eps (f y)}.
proof: Proof. intros H eps. assert (0 < eps / (@norm_factor _ V)). apply Rdiv_lt_0_compat. apply cond_pos. exact norm_factor_gt_0. destruct (unifcont_1d f a b H (mkposreal _ H0)) as [d Hd]. exists d => x y Hx Hy Hxy. specialize (Hd x y Hx Hy Hxy). apply Rnot_le_lt. contradict Hd ; contradict Hd. apply Rlt_not_le. evar_last. apply norm_compat2, Hd. simpl ; field. apply Rgt_not_eq, norm_factor_gt_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq