Theorem MeasureTheory.setIntegral_congr_set_ae

Modification history

2024-10-12 07:45

Mathlib/MeasureTheory/Integral/SetIntegral.lean

chore(MeasureTheory/Integral/SetIntegral): fix lemma names (#17658) …

Deleted MeasureTheory.setIntegral_congr_set_ae View on Github →

2024-04-18 02:39

Mathlib/MeasureTheory/Integral/SetIntegral.lean

chore: replace `set_integral` with `setIntegral` (#12215) …

Added MeasureTheory.setIntegral_congr_set_ae View on Github →