Diff — Lebesgue integral

Revision #1988 → #2600 · back to history

modifiedLebesgue integral via improper Riemann integral94efd96efb26

Field	From #1988	To #2600
mathlib.decl	MeasureTheory.AECover.integrable	MeasureTheory.AECover.integral_tendsto_of_countably_generated
provenance	ai	ai-moderated

modifiedIntegral of a complex-valued function3c46b2cdfe46

Field	From #1988	To #2600
mathlib.decl	MeasureTheory.integral_re_add_im	integral_re_add_im
provenance	ai	ai-moderated