Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.set_to_fun_congr_measure_of_add_left

Modification history

2021-12-14 14:14

src/measure_theory/integral/set_to_l1.lean

feat(measure_theory/integral/set_to_l1): various properties of the set_to_fun construction (#10713)

Added measure_theory.set_to_fun_congr_measure_of_add_left View on Github →