WIP.

Lebesgue/UniformSpace_compl.v

@@ -245,6 +245,17 @@ Lemma continuous_equiv_open :
     (forall x1, continuous f x1) <->
     (forall A2, open A2 -> open (fun x1 => A2 (f x1))).
 Proof.
+intros T1 T2 f; split; intros Hf.
+(* *)
+intros A2 HA2 x1 Hx1.
+admit.
+
+(* *)
+intros x1 A2 HA2.
+
+
+
+
 Admitted.
 
 Lemma continuous_equiv_closed :