delta epsilon proofs for continuity

Stream: new members

[Charlie Conneen]

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]

Do you mean something like metric.continuous_iff?

[Kevin Buzzard]

darn it, Patrick got there just before me.

[Kevin Buzzard]

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]

and got

Try this: exact metric.continuous_iff

[Patrick Massot]

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]

wait, you used metric.continuous_iff in that proof!

[Charlie Conneen]

Awesome, this was exactly what I was looking for!

[Patrick Massot]

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

[Charlie Conneen]

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

[Charlie Conneen]

Thanks a ton!

[Patrick Massot]

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

[Kevin Buzzard]

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]

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