Theorem MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀

Modification history

2025-01-04 12:51

Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

chore: split AEEqOfIntegral into two files, one for each integral type (#20405) …

Modified MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ View on Github →

2024-06-29 15:21

Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

chore: rename set_lintegral to setLIntegral throughout mathlib (#14260) …

Added MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ View on Github →