## Stream: new members

### Topic: Product of continuous functions

#### Heather Macbeth (May 07 2020 at 05:00):

Hello, I am still finding my way around mathlib. Where would I find that the product of two continuous functions from R to R (or in whatever greater generality) is continuous?

#### Johan Commelin (May 07 2020 at 05:04):

I think it's called continuous_mul

#### Johan Commelin (May 07 2020 at 05:05):

src/topology/algebra/monoid.lean:lemma continuous.mul [topological_space β] {f : β → α} {g : β → α}


#### Johan Commelin (May 07 2020 at 05:05):

@Heather Macbeth It has a . in the name now...

#### Johan Commelin (May 07 2020 at 05:06):

You would use it as hf.mul hg, where hf : continuous f and hg : continuous g.

Thank you!

#### Heather Macbeth (May 07 2020 at 05:21):

Would this have sufficient generality to prove that for topological vector spaces E, F and continuous functions $f : \mathbb{R} \to E$ and $g : \mathbb{R} \to F$, the tensor product $f \otimes g : \mathbb{R} \to E \otimes F$ is continuous?

#### Johan Commelin (May 07 2020 at 05:23):

Nope, it's only for functions into a topological monoid

#### Johan Commelin (May 07 2020 at 05:23):

I'm afraid that the lemma you want is not yet there. Although @Sebastien Gouezel might have proved it

#### Johan Commelin (May 07 2020 at 05:24):

I don't know that part of the library too well

#### Johan Commelin (May 07 2020 at 05:24):

We have a whole bunch of stuff on continuous multilinear maps... but that's not exactly what you want

#### Heather Macbeth (May 07 2020 at 05:25):

I guess there is a monoid (in particular, graded algebra) consisting of arbitrarily iterated tensor products of E and F? Who knows if this is sensibly topological.

#### Johan Commelin (May 07 2020 at 05:41):

I think this is not a "new members" question. You might have more luck in the "maths" stream. Hopefully an expert can help you over there.

#### Johan Commelin (May 07 2020 at 05:41):

Some people don't read this stream, because there is lot's of traffic here.

#### Johan Commelin (May 07 2020 at 05:42):

@Heather Macbeth you might want to ping Yury Kudrashov and/or Sébastien Gouëzel and/or Patrick Massot, in your new question.

#### Heather Macbeth (May 07 2020 at 05:57):

Done! Thank you.

Last updated: May 17 2021 at 21:12 UTC