theorem MeasureTheory.Adapted.progMeasurable_of_rightContinuous {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} [TopologicalSpace ι] [TopologicalSpace β] [LinearOrder ι] [TopologicalSpace.MetrizableSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [OpensMeasurableSpace ι] [TopologicalSpace.PseudoMetrizableSpace β] {mΩ : MeasurableSpace Ω} {X : ι → Ω → β} {𝓕 : Filtration ι mΩ} (h : Adapted 𝓕 X) (hu_cont : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) : ProgMeasurable 𝓕 X