proposition: Lemma extension_cont_continuous (f g : R -> U) (a : R) : continuous f a -> continuous g a -> f a = g a -> continuous (extension_cont f g a) a.
proof: Proof. simpl => Cf Cg Heq ; apply filterlim_locally => /= eps. generalize (proj1 (filterlim_locally _ _) Cf eps) => {} Cf. generalize (proj1 (filterlim_locally _ _) Cg eps) => {} Cg. generalize (filter_and _ _ Cf Cg). apply filter_imp => {Cf Cg} x [Cf Cg]. rewrite /extension_cont. case: Rle_dec (Rle_refl a) => // _ _. case: Rle_dec => // H. by rewrite Heq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv