diff --git a/Lebesgue/Set_theory/Set_system/Topology.v b/Lebesgue/Set_theory/Set_system/Topology.v
index 6b658d8ee1d465360a72c88c3fec9e4942bbf650..b7a7c85f30dcc4ef881d2345b64f2e3b8775ffcf 100644
--- a/Lebesgue/Set_theory/Set_system/Topology.v
+++ b/Lebesgue/Set_theory/Set_system/Topology.v
@@ -226,3 +226,10 @@ split; intros Hf A1 HA1; induction HA1 as [A2 HA2].
 Admitted.
 
 End Continuous_Facts1.
+
+
+(* TODO: add section(s) on UniformSpace.
+ Eg with lemmas
+    ball_is_Basisp (any center, any radius)
+    ball_seq_is_Basisp (any center, seq radius = 1 / S n)
+*)