proposition: Lemma extension_C0_continuous (f : R -> V) (a b : Rbar) : Rbar_le a b -> (forall x : R, Rbar_le a x -> Rbar_le x b -> continuous f x) -> forall x, continuous (extension_C0 f a b) x.
proof: Proof. intros Hab Cf x. apply Rbar_le_lt_or_eq_dec in Hab ; case: Hab => Hab. case: (Rbar_lt_le_dec x a) => Hax. eapply continuous_ext_loc. apply locally_interval with m_infty a. by []. by []. move => y _ Hay. rewrite /extension_C0. case: Rbar_le_dec => H. contradict H ; by apply Rbar_lt_not_le. reflexivity. apply continuous_const. apply Rbar_le_lt_or_eq_dec in Hax ; case: Hax => Hax. case: (Rbar_lt_le_dec x b) => Hbx. eapply continuous_ext_loc. apply locally_interval with a b. by []. by []. move => y Hay Hby. rewrite /extension_C0. case: Rbar_le_dec => H. case: Rbar_le_dec => H0. reflexivity. contradict H0 ; by apply Rbar_lt_le. contradict H ; by apply Rbar_lt_le. apply Cf ; by apply Rbar_lt_le. apply Rbar_le_lt_or_eq_dec in Hbx ; case: Hbx => Hbx. eapply continuous_ext_loc. apply locally_interval with b p_infty. by []. by []. move => y Hby _. rewrite /extension_C0. case: Rbar_le_dec => H. case: Rbar_le_dec => H0. contradict H0 ; by apply Rbar_lt_not_le. reflexivity. contradict H ; eapply Rbar_le_trans, Rbar_lt_le, Hby. by apply Rbar_lt_le. apply continuous_const. destruct b as [b | | ] => //. injection Hbx => {} Hbx. rewrite -Hbx {x Hbx} in Hax |- *. apply continuous_ext_loc with (extension_cont f (fun _ => f (real b)) b). apply locally_interval with a p_infty => //. move => y Hay _. rewrite /extension_cont /extension_C0. case: Rle_dec => H ; case: Rbar_le_dec => H0 ; case: (Rbar_le_dec y b) => // _. contradict H0 ; by apply Rbar_lt_le. contradict H0 ; by apply Rbar_lt_le. apply extension_cont_continuous => //. apply Cf => /=. by apply Rbar_lt_le. by apply Rle_refl. by apply continuous_const. destruct a as [a | | ] => //. injection Hax => {} Hax. rewrite -Hax {x Hax}. apply continuous_ext_loc with (extension_cont (fun _ => f (real a)) f a). apply locally_interval with m_infty b => //. move => y _ Hbx. rewrite /extension_cont /extension_C0. case: Rle_dec => H ; case: Rbar_le_dec => //= H0 ; try case: Rbar_le_dec => // H1. by replace y with a by now apply Rle_antisym. contradict H1 ; by apply Rbar_lt_le. contradict H1 ; by apply Rbar_lt_le. by contradict H0 ; apply Rlt_le, Rnot_le_lt. apply extension_cont_continuous => //. by apply continuous_const. apply Cf. by apply Rle_refl. by apply Rbar_lt_le. rewrite -Hab {b Hab Cf}. eapply continuous_ext. intros y. rewrite /extension_C0. case: Rbar_le_dec => H. 2: reflexivity. case: Rbar_le_dec => // H0. destruct a as [a | | ] => //. by replace y with a by now apply Rle_antisym. by apply continuous_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv