Uniformly Continuous on Metric Spaces

Stream: maths

[Rohan Mitta]

Have I formalised this right and is it in mathlib?

import analysis.metric_space

example {X : Type*} {Y : Type*} [metric_space X] [metric_space Y] (f : X → Y) :
uniform_continuous f ↔ ∀ ε, ε > 0 → ∃ δ (H : δ > 0), ∀ x₁ x₂ : X,
  dist x₁ x₂ < δ → dist (f x₁) (f x₂) < ε := sorry

[Johannes Hölzl]

looks good to me, and I don't think we have it in mathlib yet

[Johannes Hölzl]

sorry, just found it uniform_continuous_of_metric

[Kevin Buzzard]

Thanks Johannes!

[Patrick Massot]

Rohan, note that ∀ ε, ε > 0 can be written ∀ ε > 0 like you would do on paper

[Patrick Massot]

Lean will parse that exactly as you originally wrote

[Rohan Mitta]

Thanks everyone!

[Kenny Lau]

Lean will parse that exactly as you originally wrote

well not exactly...