Theorems · Theorem · probability

ProbabilityTheory.IsAEKolmogorovProcess.mk.congr_simp

∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p p_1 : ℝ} (e_p : p = p_1) {q q_1 : ℝ} (e_q : q = q_1) {M M_1 : NNReal}
  (e_M : M = M_1) {P P_1 : MeasureTheory.Measure Ω} (e_P : P = P_1) (X X_1 : T → Ω → E) (e_X : X = X_1)
  (h : ProbabilityTheory.IsAEKolmogorovProcess X P p q M) (a a_1 : T),
  a = a_1 →
    ∀ (a_2 a_3 : Ω),
      a_2 = a_3 →
        ProbabilityTheory.IsAEKolmogorovProcess.mk X h a a_2 = ProbabilityTheory.IsAEKolmogorovProcess.mk X_1 ⋯ a_1 a_3

Defined in

Mathlib.Probability.Process.Kolmogorov

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace