Mathlib Map

Theorems · Definition · probability

MeasureTheory.IsStoppingTime.measurableSpace

{Ω : Type u_1} →
  {ι : Type u_3} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {f : MeasureTheory.Filtration ι m} → {τ : Ω → WithTop ι} → MeasureTheory.IsStoppingTime f τ → MeasurableSpace Ω

The associated σ-algebra with a stopping time.

Defined in
Mathlib.Probability.Process.Stopping
Cited by
49 results in Mathlib
Foundations
Depth 69 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 · cited by 10IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff · cited by 6IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSet_eq' · cited by 5IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSet_le' · cited by 5IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSet_min_iff · cited by 5IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSpace_le_of_le · cited by 5IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range' · cited by 4IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time · cited by 4IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSpace_const · cited by 4IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSpace_min · cited by 4IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSpace_mono · cited by 4IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurable · cited by 3IsStoppingTime.measurableMeasureTheory.IsStoppingTime.measurableSet · cited by 3IsStoppingTime.measurable…MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff · cited by 3IsStoppingTime.measurable…MeasureTheory.measurable_stoppedValue · cited by 2MeasureTheory.measurable_…Set · cited by 53352SetMeasurableSpace · cited by 13106MeasurableSpacePreorder · cited by 7952PreorderSet.ofPred · cited by 6101Set.ofPredWithTop · cited by 3754WithTopMeasurableSet · cited by 3075MeasurableSetWithTop.some · cited by 1128WithTop.someMeasureTheory.Filtration · cited by 425MeasureTheory.FiltrationMeasureTheory.IsStoppingTime · cited by 122MeasureTheory.IsStoppingT…IsStoppingTime.measurableSpaceCITED BYCITES

Cites9

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

Cited by49

Results whose statement or proof uses this declaration.