Theorems · Theorem · probability

MeasureTheory.stoppedValue_hittingBtwn_mem

∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι]
  {u : ι → Ω → β} {s : Set β} {n m : ι} {ω : Ω},
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → MeasureTheory.stoppedValue u (fun ω => ↑(MeasureTheory.hittingBtwn u s n m ω)) ω ∈ s

Defined in

Mathlib.Probability.Process.HittingTime

Cited by

3 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderWellFoundedLT