bochner): prove `set_integral_eq_subtype` (#10858)

Commit

4 years ago

feat(measure_theory/integral/bochner): prove `set_integral_eq_subtype` (#10858) Relate integral w.r.t. `μ.restrict s` and w.r.t. `comap (coe : s → α) μ`.

Author

urkud

Parents

86493f12

mathlib3 fc09b17f - feat(measure_theory/integral/bochner): prove `set_integral_eq_subtype` (#10858)

mathlib3
fc09b17f - feat(measure_theory/integral/bochner): prove `set_integral_eq_subtype` (#10858)