Theorems · Theorem · probability
MeasureTheory.IsStoppingTime.le_measurableSpace_of_const_le
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
{τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) {i : ι}, (∀ (ω : Ω), ↑i ≤ τ ω) → ↑f i ≤ hτ.measurableSpace- Defined in
- Mathlib.Probability.Process.Stopping
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 72 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.
Cites13
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
- WithTop.somestatement and proof · cited by 1,128
- Eq.leproof · cited by 605
- MeasureTheory.Filtrationstatement and proof · cited by 425
- MeasureTheory.Filtration.seqstatement · cited by 184
- MeasureTheory.IsStoppingTimestatement and proof · cited by 122
- MeasureTheory.IsStoppingTime.measurableSpacestatement · cited by 49
- MeasureTheory.isStoppingTime_constproof · cited by 12
- MeasureTheory.IsStoppingTime.measurableSpace_constproof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.