## Stream: new members

### Topic: delta epsilon proofs for continuity

#### Charlie Conneen (May 19 2020 at 20:49):

I plan on working a bit more closely with the topology files in mathlib, and in the future will be working in the reals quite a bit. I find that working with the preimage definition can get a bit tedious, so I was wondering if there was a theorem somewhere in a nook or cranny of mathlib showing that a delta-epsilon proof is sufficient for proving continuity in the reals. I've been searching myself but can't seem to find such a theorem.

#### Patrick Massot (May 19 2020 at 20:52):

Do you mean something like metric.continuous_iff?

#### Kevin Buzzard (May 19 2020 at 20:52):

darn it, Patrick got there just before me.

#### Kevin Buzzard (May 19 2020 at 20:52):

I did this:

import topology.instances.real data.real.basic tactic

example (f : ℝ → ℝ) : continuous f ↔ ∀ x, ∀ ε > 0, ∃ δ > 0, ∀ y,
abs (y - x) < δ → abs (f y - f x) < ε := by library_search


#### Kevin Buzzard (May 19 2020 at 20:53):

and got

Try this: exact metric.continuous_iff


#### Patrick Massot (May 19 2020 at 20:53):

If you don't know the answer yet, you can go with

import topology.instances.real

example (f : ℝ → ℝ) : continuous f ↔ sorry :=
begin
simp_rw [metric.continuous_iff, real.dist_eq],
sorry
end


#### Kevin Buzzard (May 19 2020 at 20:54):

wait, you used metric.continuous_iff in that proof!

#### Charlie Conneen (May 19 2020 at 20:54):

Awesome, this was exactly what I was looking for!

#### Patrick Massot (May 19 2020 at 20:54):

Sure, because I knew the name of the lemmas, but I was too lazy to type the statement

#### Charlie Conneen (May 19 2020 at 20:55):

Also just learned about library_search. That will come in handy...

Thanks a ton!

#### Patrick Massot (May 19 2020 at 20:55):

Charlie, you should still stop worrying and learn to love general topology and filters.

#### Kevin Buzzard (May 19 2020 at 20:55):

If you're learning your way around a library, library_search is really useful. The only other skill you need is an understanding of exactly which kind of lemma one would expect to be in Lean's maths library

#### Charlie Conneen (May 19 2020 at 20:57):

Haha! No worries there, I absolutely adore general topology. I am only working with fancy spaces out of necessity...

Last updated: May 08 2021 at 04:14 UTC