Commit 2021-09-24 08:36 6a9ba186

feat(measure_theory): ι → α ≃ᵐ α if [unique ι] (#9353)

• define versions of equiv.fun_unique for order_iso and measurable_equiv;
• use the latter to relate integrals over (sets in) ι → α and α, where ι is a type with an unique element.