Theorem MeasureTheory.condexp_indicator_aux

Modification history

2023-06-30 01:46

Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean

fix: change compl precedence (#5586)

Modified MeasureTheory.condexp_indicator_aux View on Github →

2023-06-17 13:45

Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean

feat: port MeasureTheory.Function.ConditionalExpectation.Indicator (#5188)

Added MeasureTheory.condexp_indicator_aux View on Github →