using measurable_embedding

Stream: general

[Felix Weilacher]

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]

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]

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]

#17980