proposition: Lemma C0_extension_le {T : UniformSpace} (f : R -> T) (a b : R) : (forall c : R, a <= c <= b -> filterlim f (locally c) (locally (f c))) -> {g : R -> T | (forall c, filterlim g (locally c) (locally (g c))) /\ (forall c : R, a <= c <= b -> g c = f c)}.
proof: Proof. intros. case: (Rlt_le_dec a b) => Hab. destruct (C0_extension_lt f (f a) (f b) a b Hab) as [g [Cg [Gab [Ga Gb]]]]. intros c Hc. apply H ; split ; apply Rlt_le, Hc. eapply filterlim_filter_le_1, H. by apply filter_le_within. intuition. eapply filterlim_filter_le_1, H. by apply filter_le_within. intuition. exists g ; repeat split => //. intros c [Hac Hcb]. case: Hac => [ Hac | <-] //. case: Hcb => [ Hcb | ->] //. apply Gab ; by split. exists (fun _ => f a) ; split ; simpl. move => c. by apply filterlim_const. intros c [Hac Hca]. case: Hab => Hab. contradict Hab ; apply Rle_not_lt. by apply Rle_trans with c. rewrite Hab in Hca. by apply f_equal, Rle_antisym. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq