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