Zulip Chat Archive

Stream: new members

Topic: Product of continuous functions


view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 07 2020 at 05:04):

I think it's called continuous_mul

view this post on Zulip Johan Commelin (May 07 2020 at 05:05):

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

view this post on Zulip Johan Commelin (May 07 2020 at 05:05):

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

view this post on Zulip Johan Commelin (May 07 2020 at 05:06):

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

view this post on Zulip Heather Macbeth (May 07 2020 at 05:13):

Thank you!

view this post on Zulip 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:REf : \mathbb{R} \to E and g:RFg : \mathbb{R} \to F, the tensor product fg:REFf \otimes g : \mathbb{R} \to E \otimes F is continuous?

view this post on Zulip Johan Commelin (May 07 2020 at 05:23):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 07 2020 at 05:24):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 07 2020 at 05:41):

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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (May 07 2020 at 05:57):

Done! Thank you.


Last updated: May 17 2021 at 21:12 UTC