Theorem measure_theory.with_densityᵥ_eq_with_density_pos_part_sub_with_density_neg_part
Modification history
2021-09-16 11:34
src/measure_theory/measure/with_density_vector_measure.lean
feat(measure_theory/measure/with_density_vector_measure): `with_densityᵥ` of a real function equals the density of the pos part - density of the neg part (#9215)
Added measure_theory.with_densityᵥ_eq_with_density_pos_part_sub_with_density_neg_partView on Github →