mathlib
1b235421 - feat(measure_theory/integral): generalize some integral properties to set_to_fun (#15423)

Commit

3 years ago

feat(measure_theory/integral): generalize some integral properties to set_to_fun (#15423) Now those lemmas can be applied to the conditional expectation as well.

Author

RemyDegenne

Parents

5a6671a7

mathlib 1b235421 - feat(measure_theory/integral): generalize some integral properties to set_to_fun (#15423)

mathlib
1b235421 - feat(measure_theory/integral): generalize some integral properties to set_to_fun (#15423)