# Zulip Chat Archive

## Stream: general

### Topic: formulating continuity lemmas

#### Oliver Nash (Nov 05 2021 at 11:33):

@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 (Nov 05 2021 at 11:34):

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 (Nov 05 2021 at 11:37):

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

#### Eric Wieser (Nov 05 2021 at 11:37):

Why is that question silly?

#### Oliver Nash (Nov 05 2021 at 11:37):

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

#### Eric Wieser (Nov 05 2021 at 11:38):

Oh, I thought your question was about using `(λ x, f x + g x)`

vs `f + g`

in the statement.

#### Oliver Nash (Nov 05 2021 at 11:38):

Nope!

#### Floris van Doorn (Nov 05 2021 at 12:02):

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 (Nov 05 2021 at 12:19):

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 (Nov 05 2021 at 12:22):

Is this a feature of a limitation of `continuity`

?

#### Floris van Doorn (Nov 05 2021 at 12:33):

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

Last updated: Aug 03 2023 at 10:10 UTC