Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.measure.restrict_prod_eq_prod_univ

Modification history

2021-11-10 14:52
src/measure_theory/constructions/prod.lean
feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions (#10241) …
Modified measure_theory.measure.restrict_prod_eq_prod_univView on Github →
2021-02-07 23:41
src/measure_theory/prod.lean
feat(measure_theory/lebesgue_measure): integral as volume between graphs (#5932) …
Added measure_theory.measure.restrict_prod_eq_prod_univView on Github →