WIP: equiv defs to prove.

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.