Product of continuous functions

Stream: new members

[Heather Macbeth]

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]

I think it's called continuous_mul

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Heather Macbeth]

Thank you!

[Heather Macbeth]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Heather Macbeth]

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]

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]

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

[Johan Commelin]

@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]

Done! Thank you.