formulating continuity lemmas

Stream: general

[Oliver Nash]

@Floris van Doorn I was just looking at your remarks here https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/formulating.20continuity.20lemmas as well as the corresponding library note.

[Oliver Nash]

For example, should we therefore add the following:

import topology.algebra.module

variables {α β M : Type*} [topological_space α] [topological_space β] [topological_space M]
variables {f g : α → β} (hf : continuous f) (hg : continuous g) (t : M)

@[simp] lemma continuous_add' [has_add β] [has_continuous_add β] :
  continuous (f + g) :=
(@continuous_add β _ _ _).comp $ hf.prod_mk hg

@[simp] lemma continuous_sub' [has_sub β] [has_continuous_sub β] :
  continuous (f - g) :=
(@continuous_sub β _ _ _).comp $ hf.prod_mk hg

@[simp] lemma continuous_neg' [add_group β] [topological_add_group β] :
  continuous (-f) :=
continuous_neg.comp hf

@[simp] lemma continuous_smul' [has_scalar M β] [has_continuous_smul M β] :
  continuous (t • f) :=
(@continuous_smul M β _ _ _ _).comp (continuous_const.prod_mk hf)

[Oliver Nash]

Oh wait, I think I'm being silly. Ignore!

[Eric Wieser]

Why is that question silly?

[Oliver Nash]

Well for one thing, I had forgotten that we have docs#continuous.add etc

[Eric Wieser]

Oh, I thought your question was about using (λ x, f x + g x) vs f + g in the statement.

[Oliver Nash]

Nope!

[Floris van Doorn]

Yeah, we have the versions like docs#continuous.add. I don't think it matters too much whether we formulate with (λ x, f x + g x) vs f + g (that distinction matters for rw and simp, but these continuity proofs are usually proven using term-mode)

[Reid Barton]

I think continuity uses the reducible transparency level by default, in which case you would want the lemma statement to syntactically match whatever you have, which is most often the form with the lambda

[Oliver Nash]

Is this a feature of a limitation of continuity?

[Floris van Doorn]

Probably a necessary feature. Otherwise it would spend too much time unfolding definitions.