Theorems · Theorem · probability
MeasureTheory.IsStoppingTime.measurableSpace_le
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ), hτ.measurableSpace ≤ m- Defined in
- Mathlib.Probability.Process.Stopping
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- Preorderstatement and proof · cited by 7,952
- WithTopstatement and proof · cited by 3,754
- LE.le.transproof · cited by 3,151
- MeasureTheory.Filtrationstatement and proof · cited by 425
- iSup_leproof · cited by 190
- MeasureTheory.IsStoppingTimestatement and proof · cited by 122
- MeasureTheory.Filtration.leproof · cited by 65
- MeasureTheory.IsStoppingTime.measurableSpacestatement · cited by 49
- MeasureTheory.IsStoppingTime.measurableSpace_le'proof · cited by 2
Cited by10
Results whose statement or proof uses this declaration.
- MeasureTheory.IsStoppingTime.measurable'proof · cited by 1
- MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_rangestatement and proof · cited by 1
- MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_lestatement and proof · cited by 1
- MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_lestatement and proof · cited by 1
- MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_lestatement and proof · cited by 1
- MeasureTheory.condExp_stopping_time_ae_eq_restrict_eqstatement and proof · cited by 0
- MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countablestatement and proof · cited by 0
- MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_conststatement and proof · cited by 0
- MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExpstatement and proof · cited by 0
- MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_conststatement and proof · cited by 0