@[simp]

theorem MeasureTheory.stoppedProcess_const {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u₀ : Ω → β} {τ : Ω → WithTop ι} : stoppedProcess (fun (x : ι) => u₀) τ = fun (x : ι) => u₀

@[simp]

theorem MeasureTheory.stoppedProcess_neg {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Neg β] {u : ι → Ω → β} {τ : Ω → WithTop ι} : stoppedProcess (-u) τ = -stoppedProcess u τ

@[simp]

theorem MeasureTheory.stoppedProcess_add {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Add β] {u v : ι → Ω → β} {τ : Ω → WithTop ι} : stoppedProcess (u + v) τ = stoppedProcess u τ + stoppedProcess v τ

@[simp]

theorem MeasureTheory.stoppedProcess_sub {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Sub β] {u v : ι → Ω → β} {τ : Ω → WithTop ι} : stoppedProcess (u - v) τ = stoppedProcess u τ - stoppedProcess v τ

@[simp]

theorem MeasureTheory.stoppedProcess_const_smul {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [SMul ℝ β] (c : ℝ) {u : ι → Ω → β} {τ : Ω → WithTop ι} : stoppedProcess (c • u) τ = c • stoppedProcess u τ

@[simp]

theorem MeasureTheory.stoppedProcess_const_bot {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] [OrderBot ι] {E : Type u_4} (X : ι → Ω → E) : (stoppedProcess X fun (x : Ω) => ⊥) = fun (x : ι) => X ⊥

@[simp]

theorem MeasureTheory.stoppedProcess_const_top {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {E : Type u_4} (X : ι → Ω → E) : (stoppedProcess X fun (x : Ω) => ⊤) = X