Constructive uniformities of pseudometrics and Bishop topologies1

IOSIF PETRAKIS

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.

theorem extraabs (a : ℝ) (h : 0 < a) : 1 ≤ |1 + a|

theorem Hδ (δ : ℝ) (hδ : 0 < δ) : 1 ≤ |δ * δ⁻¹ + δ ^ 2 * (1 / 4)|

Lemma by Clark Eggerman.