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

theorem MeasureTheory.stoppedProcess_indicator_comm {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Zero β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {s : Set Ω} (i : ι) : stoppedProcess (fun (i : ι) => s.indicator (u i)) τ i = s.indicator (stoppedProcess u τ i)

theorem MeasureTheory.stoppedProcess_indicator_comm' {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} [Zero β] {u : ι → Ω → β} {τ : Ω → WithTop ι} {s : Set Ω} : stoppedProcess (fun (i : ι) => s.indicator (u i)) τ = fun (i : ι) => s.indicator (stoppedProcess u τ i)

theorem MeasureTheory.stoppedValue_stoppedProcess_apply {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {ω : Ω} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} (hω : σ ω ≠ ⊤) : stoppedValue (stoppedProcess u τ) σ ω = stoppedValue u (fun (ω : Ω) => min (σ ω) (τ ω)) ω

@[simp]

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

theorem MeasureTheory.stoppedProcess_stoppedProcess' {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} : stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u fun (ω : Ω) => min (σ ω) (τ ω)

theorem MeasureTheory.stoppedProcess_stoppedProcess_of_le_right {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} (h : σ ≤ τ) : stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u σ

theorem MeasureTheory.stoppedProcess_stoppedProcess_of_le_left {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ σ : Ω → WithTop ι} (h : τ ≤ σ) : stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u τ

theorem MeasureTheory.stoppedProcess_eq_stoppedValue_apply {ι : Type u_1} {Ω : Type u_2} [Nonempty ι] [LinearOrder ι] {β : Type u_4} {u : ι → Ω → β} {τ : Ω → WithTop ι} (i : ι) (ω : Ω) : stoppedProcess u τ i ω = stoppedValue u (fun (ω : Ω) => min (↑i) (τ ω)) ω