TODO: link with UniformSpace.

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)
+*)