Theorems · Theorem · probability

ProbabilityTheory.Locally.congr_simp

∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [inst : LinearOrder ι] [inst_1 : OrderBot ι]
  [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E] (p p_1 : (ι → Ω → E) → Prop),
  p = p_1 →
    ∀ (𝓕 𝓕_1 : MeasureTheory.Filtration ι mΩ),
      𝓕 = 𝓕_1 →
        ∀ (X X_1 : ι → Ω → E),
          X = X_1 →
            ∀ (P P_1 : MeasureTheory.Measure Ω),
              P = P_1 → ProbabilityTheory.Locally p 𝓕 X P = ProbabilityTheory.Locally p_1 𝓕_1 X_1 P_1

Defined in

Mathlib.Probability.Process.LocalProperty

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderOrderBotTopologicalSpaceOrderTopologyZero