Theorems · Theorem · probability

MeasureTheory.isStoppingTime_piecewise_const

∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {𝒢 : MeasureTheory.Filtration ι m} {i j : ι}
  {s : Set Ω} [inst_1 : DecidablePred fun x => x ∈ s],
  i ≤ j → MeasurableSet s → MeasureTheory.IsStoppingTime 𝒢 (s.piecewise (fun x => ↑i) fun x => ↑j)

Defined in

Mathlib.Probability.Process.Stopping

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderDecidablePred