Zulip Chat Archive

Stream: general

Topic: using measurable_embedding

Felix Weilacher (Dec 18 2022 at 21:50):

Don't the hypotheses on f in docs#measurable_equiv.set.image and docs#measurable_equiv.set.range exactly say that f is a measurable_embedding? Should the statements be changed to use this bundled name?

Felix Weilacher (Dec 19 2022 at 02:01):

after poking around I found docs#measurable_embedding.equiv_range which seems to be the same as docs#measurable_equiv.set.range except that it does use measurable_embedding, but the two results do not reference each other. They essentially repeat the argument.

Rémy Degenne (Dec 19 2022 at 07:19):

I looked at git blame and apparently docs#measurable_equiv.set.range predates measurable_embedding. I guess that it should have been changed but was missed, and a new docs#measurable_embedding.equiv_range was written instead. A PR removing the old stuff or changing it to use measurable_embedding would be welcome.

Felix Weilacher (Dec 20 2022 at 01:59):


Last updated: Aug 03 2023 at 10:10 UTC