Commit 2023-10-26 21:10 c09b9895

View on Github →

feat(MeasureTheory/Integral/Lebesgue): add set_lintegral_subtype (#7679)

  • Add MeasureTheory.set_lintegral_eq_subtype and MeasureTheory.set_lintegral_subtype.
  • Add MeasurableEmbedding.comap_map, MeasurableEmbedding.comap_restrict, and MeasurableEmbedding.restrict_comap.
  • Drop measurability assumption in MeasurableEmbedding.comap_preimage.
  • Remove some empty lines.

Estimated changes