Theorem MeasureTheory.AEStronglyMeasurable'.neg

Modification history

2025-08-14 19:32
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
chore: remove >6 month old deprecations (#28370) …
Deleted MeasureTheory.AEStronglyMeasurable'.negView on Github →
2025-04-09 09:39
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
feat: generalize Mathlib.MeasureTheory (#23147) …
Modified MeasureTheory.AEStronglyMeasurable'.negView on Github →
2025-02-16 15:19
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)
Modified MeasureTheory.AEStronglyMeasurable'.negView on Github →
2025-01-25 09:32
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
refactor: merge `AEStronglyMeasurable` and `AEStronglyMeasurable'` (#20932) …
Modified MeasureTheory.AEStronglyMeasurable'.negView on Github →
2023-06-13 09:59
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
feat: port MeasureTheory.Function.ConditionalExpectation.AEMeasurable (#5005)
Added MeasureTheory.AEStronglyMeasurable'.negView on Github →