Zulip Chat Archive
Stream: maths
Topic: measure_equiv
Yury G. Kudryashov (Sep 22 2021 at 12:36):
I think about introducing measure_equiv α β μ ν
. It will extend measurable_equiv
and add map e μ = ν
. Any objections?
Yury G. Kudryashov (Sep 22 2021 at 12:39):
(with special notation-level support for measure_equiv α β volume volume
)
Last updated: Dec 20 2023 at 11:08 UTC