Zulip Chat Archive

Stream: new members

Topic: delta epsilon proofs for continuity


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

view this post on Zulip Patrick Massot (May 19 2020 at 20:52):

Do you mean something like metric.continuous_iff?

view this post on Zulip Kevin Buzzard (May 19 2020 at 20:52):

darn it, Patrick got there just before me.

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

view this post on Zulip Kevin Buzzard (May 19 2020 at 20:53):

and got

Try this: exact metric.continuous_iff

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

view this post on Zulip Kevin Buzzard (May 19 2020 at 20:54):

wait, you used metric.continuous_iff in that proof!

view this post on Zulip Charlie Conneen (May 19 2020 at 20:54):

Awesome, this was exactly what I was looking for!

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

view this post on Zulip Charlie Conneen (May 19 2020 at 20:55):

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

view this post on Zulip Charlie Conneen (May 19 2020 at 20:55):

Thanks a ton!

view this post on Zulip Patrick Massot (May 19 2020 at 20:55):

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

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

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