Mathlib v3 is deprecated. Go to Mathlib v4

Def measure_theory.finite_measure.restrict

Modification history

2022-11-26 00:19
src/measure_theory/measure/finite_measure.lean
feat(measure_theory/measure/probability_measure): Add a bit of simple API to probability_measure. (#17610) …
Added measure_theory.finite_measure.restrictView on Github →