proposition: Lemma continuous_C_id_2 (x : C) : continuous (T := AbsRing_UniformSpace C_AbsRing) (U := C_UniformSpace) (fun y => y) x.
proof: Proof. intros P HP. by apply locally_C. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)