Commit 2025-04-15 08:42 6b8c3cca

View on Github →

chore: split MeasureTheory.Integral.SetIntegral (#24070) Split off

  • MeasureTheory.Integral.Bochner.ContinuousLinearMap for the commuting of continuous linear maps with the Bochner integral
  • MeasureTheory.Integral.Bochner.FundThmCalculus for the fundamental theorem of calculus on set integrals The file itself is also renamed to MeasureTheory.Integral.Bochner.Set.

Estimated changes

added theorem fst_integral
added theorem integral_conj
added theorem integral_im
added theorem integral_ofReal
added theorem integral_pair
added theorem integral_re
added theorem integral_re_add_im
added theorem integral_smul_const
added theorem setIntegral_re_add_im
added theorem snd_integral
added theorem swap_integral
deleted theorem fst_integral
deleted theorem integral_complex_ofReal
deleted theorem integral_conj
deleted theorem integral_im
deleted theorem integral_ofReal
deleted theorem integral_pair
deleted theorem integral_re
deleted theorem integral_re_add_im
deleted theorem integral_smul_const
deleted theorem setIntegral_re_add_im
deleted theorem snd_integral
deleted theorem swap_integral