theorem MeasureTheory.stoppedProcess_min_eq_stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Nonempty ι] [LinearOrder ι] (X : ι → Ω → E) (τ : Ω → WithTop ι) {i j : ι} (hij : i ≤ j) : stoppedProcess X (fun (ω : Ω) => min (↑j) (τ ω)) i = stoppedProcess X τ i

theorem WithTop.biInf_le_coe_iff_of_nhdsGT_eq_bot {ι : Type u_1} {κ : Type u_2} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {s : Set κ} {x : κ → WithTop ι} {i : ι} (hi : nhdsWithin i (Set.Ioi i) = ⊥) : ⨅ n ∈ s, x n ≤ ↑i ↔ ∃ n ∈ s, x n ≤ ↑i

If i is isolated on its right, an infimum of elements of WithTop ι is at most i iff one of them is.

theorem MeasureTheory.IsStoppingTime.biInf' {ι : Type u_1} {Ω : Type u_2} {κ : Type u_3} {m : MeasurableSpace Ω} [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {f : Filtration ι m} {τ : κ → Ω → WithTop ι} {s : Set κ} (hs : s.Countable) [f.IsRightContinuous] (hτ : ∀ n ∈ s, IsStoppingTime f (τ n)) : IsStoppingTime f fun (ω : Ω) => ⨅ n ∈ s, τ n ω

The infimum of countably many stopping times with respect to a right-continuous filtration is a stopping time. This is IsStoppingTime.biInf without the hypotheses DenselyOrdered and NoMaxOrder: at a time which is isolated on its right, the infimum is attained.