mathlib3 documentation


Lebesgue measure on #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define Lebesgue measure on . Since is defined as a structure as the push-forward of the volume on ℝ² under the natural isomorphism. There are (at least) two frequently used ways to represent ℝ² in mathlib: ℝ × ℝ and fin 2 → ℝ. We define measurable equivalences (measurable_equiv) to both types and prove that both of them are volume preserving (in the sense of measure_theory.measure_preserving).