proposition: Lemma continuous_C (f : C -> C) (x : C) : continuous (T := C_UniformSpace) (U := C_UniformSpace) f x <-> continuous (T := AbsRing_UniformSpace C_AbsRing) (U := AbsRing_UniformSpace C_AbsRing) f x.
proof: Proof. split => H. - intros P HP. by apply locally_C, H, locally_C. - intros P HP. by apply locally_C, H, locally_C. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)