Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-14 11:12 88ba31c9

View on Github →

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.

Estimated changes

Modified src/logic/equiv/fin.lean

added def equiv.pi_fin_succ_above_equiv

added def order_iso.pi_fin_succ_above_iso

Modified src/logic/equiv/set.lean

added theorem equiv.preimage_pi_equiv_pi_subtype_prod_symm_pi

Modified src/measure_theory/constructions/pi.lean

deleted theorem measure_theory.measure.map_pi_equiv_pi_subtype_prod

deleted theorem measure_theory.measure.map_pi_equiv_pi_subtype_prod_symm

added theorem measure_theory.measure_preserving_pi_equiv_pi_subtype_prod

added theorem measure_theory.measure_preserving_pi_fin_succ_above_equiv

added theorem measure_theory.volume_preserving_pi_equiv_pi_subtype_prod

added theorem measure_theory.volume_preserving_pi_fin_succ_above_equiv

Modified src/measure_theory/measurable_space.lean

added def measurable_equiv.pi_equiv_pi_subtype_prod

added def measurable_equiv.pi_fin_succ_above_equiv

Modified src/measure_theory/measure/lebesgue.lean

deleted theorem real.map_transvection_volume_pi

added theorem real.volume_preserving_transvection_struct