diff --git a/Lebesgue/UniformSpace_compl.v b/Lebesgue/UniformSpace_compl.v
index 66da3b5ac947db0c5795fda0af7ff1a3d29ea67c..f8c79ac0f2c64a1c8bc9b7ae998fda9f8389ba46 100644
--- a/Lebesgue/UniformSpace_compl.v
+++ b/Lebesgue/UniformSpace_compl.v
@@ -240,6 +240,20 @@ intros y [Hy1 Hy2]; split; [apply He1b | apply He2b];
     apply ball_le with e; try easy; [apply Rmin_l | apply Rmin_r].
 Qed.
 
+Lemma continuous_equiv_open :
+  forall {T1 T2 : UniformSpace} (f : T1 -> T2),
+    (forall x1, continuous f x1) <->
+    (forall A2, open A2 -> open (fun x1 => A2 (f x1))).
+Proof.
+Admitted.
+
+Lemma continuous_equiv_closed :
+  forall {T1 T2 : UniformSpace} (f : T1 -> T2),
+    (forall x1, continuous f x1) <->
+    (forall A2, closed A2 -> closed (fun x1 => A2 (f x1))).
+Proof.
+Admitted.
+
 End UniformSpace_compl.