@[simp]

theorem MeasureTheory.stoppedValue.add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] [Add E] {u v : ι → Ω → E} {τ : Ω → WithTop ι} : stoppedValue (u + v) τ = stoppedValue u τ + stoppedValue v τ

@[simp]

theorem MeasureTheory.stoppedValue.neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] [Neg E] {u : ι → Ω → E} {τ : Ω → WithTop ι} : stoppedValue (-u) τ = -stoppedValue u τ

@[simp]

theorem MeasureTheory.stoppedValue.sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] [Sub E] {u v : ι → Ω → E} {τ : Ω → WithTop ι} : stoppedValue (u - v) τ = stoppedValue u τ - stoppedValue v τ