## Stream: maths

### Topic: Uniformly Continuous on Metric Spaces

#### Rohan Mitta (Sep 26 2018 at 11:32):

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 (Sep 26 2018 at 11:34):

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

#### Johannes Hölzl (Sep 26 2018 at 11:34):

sorry, just found it uniform_continuous_of_metric

Thanks Johannes!

#### Patrick Massot (Sep 26 2018 at 12:05):

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

#### Patrick Massot (Sep 26 2018 at 12:06):

Lean will parse that exactly as you originally wrote

Thanks everyone!

#### Kenny Lau (Sep 26 2018 at 13:17):

Lean will parse that exactly as you originally wrote

well not exactly...

Last updated: May 10 2021 at 06:13 UTC