English
For filtrations indexed by a discrete order, Adapted and ProgMeasurable are equivalent; Adapted implies ProgMeasurable.
Русский
Для фильтраций с дискретной шкалой порядок эквивалентности: адаптированность ↔ прогрессивная измеримость; адаптированность влечёт прогрессивную измеримость.
LaTeX
$$$\\text{(Discrete ι)} \\; (h : \\mathrm{Adapted}(f,u)) \\Rightarrow \\mathrm{ProgMeasurable}(f,u)$$$
Lean4
/-- For filtrations indexed by a discrete order, `Adapted` and `ProgMeasurable` are equivalent.
This lemma provides `Adapted f u → ProgMeasurable f u`.
See `ProgMeasurable.adapted` for the reverse direction, which is true more generally. -/
theorem progMeasurable_of_discrete [TopologicalSpace ι] [DiscreteTopology ι] [SecondCountableTopology ι]
[MeasurableSpace ι] [OpensMeasurableSpace ι] [PseudoMetrizableSpace β] (h : Adapted f u) : ProgMeasurable f u :=
h.progMeasurable_of_continuous fun _ => continuous_of_discreteTopology
