Theorems · Theorem · probability

ProbabilityTheory.IsLocalizingSequence.mono

∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : ℕ → Ω → WithTop ι}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsLocalizingSequence._auto_1},
  ProbabilityTheory.IsLocalizingSequence 𝓕 τ P → ∀ᵐ (ω : Ω) ∂P, Monotone fun x => τ x ω

Defined in

Mathlib.Probability.Process.LocalProperty

Cited by

1 results in Mathlib

Foundations

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

Assumes

PreorderTopologicalSpaceOrderTopology