Theorem MeasureTheory.AEStronglyMeasurable'.of_subsingleton'

Modification history

2025-08-14 19:32
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
chore: remove >6 month old deprecations (#28370) …
Deleted MeasureTheory.AEStronglyMeasurable'.of_subsingleton'View on Github →
2025-01-25 09:32
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
refactor: merge `AEStronglyMeasurable` and `AEStronglyMeasurable'` (#20932) …
Modified MeasureTheory.AEStronglyMeasurable'.of_subsingleton'View on Github →
2024-08-25 12:38
Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
feat: remove `Nonempty` assumption in `condexpKernel` (#16138)
Added MeasureTheory.AEStronglyMeasurable'.of_subsingleton'View on Github →