Zulip Chat Archive

Stream: maths

Topic: Uniformly Continuous on Metric Spaces


view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Sep 26 2018 at 11:34):

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

view this post on Zulip Johannes Hölzl (Sep 26 2018 at 11:34):

sorry, just found it uniform_continuous_of_metric

view this post on Zulip Kevin Buzzard (Sep 26 2018 at 11:38):

Thanks Johannes!

view this post on Zulip Patrick Massot (Sep 26 2018 at 12:05):

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

view this post on Zulip Patrick Massot (Sep 26 2018 at 12:06):

Lean will parse that exactly as you originally wrote

view this post on Zulip Rohan Mitta (Sep 26 2018 at 12:14):

Thanks everyone!

view this post on Zulip 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