Mathlib Map

Theorems · Theorem · probability

MeasureTheory.IsStoppingTime.measurableSpace_le_of_le_const

∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) {i : ι}, (∀ (ω : Ω), τ ω ≤ ↑i) → hτ.measurableSpace ≤ ↑f i
Defined in
Mathlib.Probability.Process.Stopping
Cited by
2 results in Mathlib
Foundations
Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.IsStoppingTime.measurableSpace_le_of_le · cited by 5IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurable_of_le · cited by 3IsStoppingTime.measurable…MeasurableSpace · cited by 13106MeasurableSpacePreorder · cited by 7952PreorderWithTop · cited by 3754WithTopLE.le.trans · cited by 3151le.transWithTop.some · cited by 1128WithTop.someEq.le · cited by 605Eq.leMeasureTheory.Filtration · cited by 425MeasureTheory.FiltrationMeasureTheory.Filtration.seq · cited by 184Filtration.seqMeasureTheory.IsStoppingTime · cited by 122MeasureTheory.IsStoppingT…MeasureTheory.IsStoppingTime.measurableSpace · cited by 49IsStoppingTime.measurable…MeasureTheory.isStoppingTime_const · cited by 12MeasureTheory.isStoppingT…MeasureTheory.IsStoppingTime.measurableSpace_const · cited by 4IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSpace_mono · cited by 4IsStoppingTime.measurable…IsStoppingTime.measurableSpac…CITED BYCITES

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.