@[simp]

theorem MeasureTheory.stoppedValue_comp {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] {F : Type u_4} {u : ι → Ω → E} {τ : Ω → WithTop ι} {f : E → F} : stoppedValue (fun (t : ι) (ω : Ω) => f (u t ω)) τ = f ∘ stoppedValue u τ

theorem MeasureTheory.stoppedValue_norm {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] [SeminormedAddCommGroup E] {u : ι → Ω → E} {τ : Ω → WithTop ι} : stoppedValue (fun (t : ι) (ω : Ω) => ‖u t ω‖) τ = fun (ω : Ω) => ‖stoppedValue u τ ω‖

@[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