Theorems · Theorem · probability

MeasureTheory.stoppedProcess_indicator_comm

∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Zero β] {s : Set Ω} (i : ι),
  MeasureTheory.stoppedProcess (fun i => s.indicator (u i)) τ i = s.indicator (MeasureTheory.stoppedProcess u τ i)

Defined in

Mathlib.Probability.Process.Stopping

Cited by

2 results in Mathlib

Foundations

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

Assumes

NonemptyLinearOrderZero