∀ {Ω : Type u_3} {ι : Type u_4} {m : MeasurableSpace Ω} [inst : PartialOrder ι] (𝓕 : MeasureTheory.Filtration ι m),
  𝓕.rightCont =
    { seq := fun i => if (nhdsWithin i (Set.Ioi i)).NeBot then ⨅ j, ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i, mono' := ⋯,
      le' := ⋯ }