Theorems · Theorem · probability

MeasureTheory.StronglyAdapted.progMeasurable_of_continuous

Deprecated since 2026-04-24Use MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous instead.

∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : TopologicalSpace ι]
  [TopologicalSpace.MetrizableSpace ι] [SecondCountableTopology ι] [inst_5 : MeasurableSpace ι] [OpensMeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.StronglyAdapted f u → (∀ (ω : Ω), Continuous fun i => u i ω) → MeasureTheory.IsStronglyProgressive f u

Alias of MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous. A continuous and strongly adapted process is strongly progressive.

Defined in

Mathlib.Probability.Process.Adapted

Cited by

0 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderTopologicalSpaceTopologicalSpaceTopologicalSpace.MetrizableSpaceSecondCountableTopologyMeasurableSpaceOpensMeasurableSpaceTopologicalSpace.PseudoMetrizableSpace