∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ →
    ∀ (s : Set Ω),
      (MeasurableSet s ∧ ∀ (i : ι), MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})) →
        MeasurableSet sᶜ ∧ ∀ (i : ι), MeasurableSet (sᶜ ∩ {ω | τ ω ≤ ↑i})