Sum of two continuous functions is continuous

Stream: new members

[Martin C. Martin]

My mathlib search fu is weak. How do I find the name of that theorem?

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Analysis.Calculus.Deriv.Pow
import Mathlib.Analysis.Calculus.MeanValue

import Mathlib.Analysis.SpecialFunctions.Pow.Continuity

import Mathlib.Topology.Basic


example {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) :
  Continuous (f + g) := by
  library_search

I included a bunch of irrelevant files, in the hope that they would transitively include whatever file has the theorem I'm looking for.

library_search gives suggestions. In fact, it gives about 20 screen fulls of suggestions! I looked through the first few screens, none seemed to be what I wanted.

Using tab completion on continuous_add produces a short list, none of which seems to be what I want.

The equivalent theorem for derivatives is deriv_add, so I'm surprised continuous_add isn't what I want. The theorem that a constant function is continuous is continuous_const, so I would have thought that continuous_add was a winner. add_continuous also came up empty.

I looked through Mathlib/Topology/Basic.lean, but it didn't seem to be in there. Maybe I haven't included the correct file?

So, two questions:

1. How can I complete the proof above?
2. More importantly, how could I have found it on my own?

[Eric Wieser]

The answer to the first is (docs#Continuous.add)

example {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) :
  Continuous (f + g) := hf.add hg

[Martin C. Martin]

Ah, so it's Continuous.add. I forgot about theorems as fields of main definitions. Thanks.

[Jireh Loreaux]

Did exact? not find it because it was beta reduced?

[Jireh Loreaux]

Wait, Martin, library_search is old. Maybe you want to update Mathlib?

[Martin C. Martin]

Jireh Loreaux said:

Wait, Martin, library_search is old. Maybe you want to update Mathlib?

My commit is from 3 weeks ago, so not too old. It's my searching abilities that need to be updated. :)

So apply? is the new library_search? In general, any advice for searching? I can guess parts of the name, put _ between them and use tab completion. I can "go to definition" and look through source files. Anything else?

[Martin C. Martin]

Does exact? look through the context, or just look at the goal?

[Martin C. Martin]

Also, I see the @[continuity] attribute, what's that? Is there a continuity tactic?

[Michael Rothgang]

Some answers; the experts can add more.

• IIUC, library_search was split into exact?, apply and rw?. Each will look for a single lemma/theorem to apply to the given tactic. So, in principle exact? and apply? should both work here; don't know about the subtle differences.
• yup, there is a continuity tactic. (That list of tactics is not up to date, though.)

[Michael Rothgang]

Three more tricks for searching:

• look at the API docs, especially for that concept. Try to search that page. (Say, on the continuity page, looking for "add" or so. (Sometimes, lemmas are misnamed/named differently from what you thing.)
• Use loogle.lean-fro.org/, or moogle.ai/ (uses natural language).
• The new rw_search (searches for a chain of multiple rewrites, not just one lemma) and hint tactics (tries several tactics in parallel, including simp, aesop, intros, exact? and decide in parallel) can also be handy.