Theorem MeasureTheory.AEStronglyMeasurable'.mono

Modification history

2024-05-26 08:52

Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

chore(MeasureTheory): drop `autoImplicit true` (#13231)

Modified MeasureTheory.AEStronglyMeasurable'.mono View on Github →

2023-08-14 12:56

Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

feat(Probability/Kernel/Condexp): some properties of condexpKernel (#6109) …

Added MeasureTheory.AEStronglyMeasurable'.mono View on Github →