Constructive uniformities of pseudometrics and Bishop topologies #
discusses uniformities. Lean's Mathlib uses uniform spaces quite a bit. Consequently, here we use uniformities to prove that x^2 is not uniformly continuous.
discusses uniformities. Lean's Mathlib uses uniform spaces quite a bit. Consequently, here we use uniformities to prove that x^2 is not uniformly continuous.