mathlib

88ba31c9 - feat(measure_theory/constructions/pi): more `measure_preserving` lemmas (#13404)

feat(measure_theory/constructions/pi): more `measure_preserving` lemmas (#13404) * Reformulate `map_pi_equiv_pi_subtype_prod` in terms of `measure_preserving`. * Add more equivalences (bare equivalences, order isomorphisms, and measurable equivalences) on pi types.