Theorems · Definition · probability

ProbabilityTheory.IsLocalizingSequence.recOn

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

Defined in

Mathlib.Probability.Process.LocalProperty

Cited by

0 results in Mathlib

Foundations

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

Assumes

PreorderTopologicalSpaceOrderTopology