proposition: Lemma locally_C x P : locally (T := C_UniformSpace) x P <-> locally (T := AbsRing_UniformSpace C_AbsRing) x P.
proof: Proof. split => [[e He] | [e He]]. - exists e => /= y Hy. apply He. split. eapply Rle_lt_trans, Hy. eapply Rle_trans, Rmax_Cmod. apply Rmax_l. eapply Rle_lt_trans, Hy. eapply Rle_trans, Rmax_Cmod. apply Rmax_r. - assert (Hd : 0 < e / sqrt 2). apply Rdiv_lt_0_compat. by apply e. apply Rlt_sqrt2_0. exists (mkposreal _ Hd) => /= y [Hy1 Hy2]. apply He. eapply Rle_lt_trans. apply Cmod_2Rmax. rewrite Rmult_comm ; apply Rlt_div_r. apply Rlt_sqrt2_0. apply Rmax_case. by apply Hy1. by apply Hy2. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy