congr — Mathlib

English

If X and Y are ae-equal at every time t, then IsAEKolmogorovProcess X P p q M implies IsAEKolmogorovProcess Y P p q M.

Русский

Если X и Y равны почти повсюду для каждого времени t, то свойство AEKolmogorov-процесса переносится на Y.

LaTeX

$$$(\\forall t, X_t =_{a.e.} Y_t) \\Rightarrow (IsAEKolmogorovProcess X P p q M \\Rightarrow IsAEKolmogorovProcess Y P p q M)$$$

Lean4

theorem congr {Y : T → Ω → E} (hX : IsAEKolmogorovProcess X P p q M) (h : ∀ t, X t =ᵐ[P] Y t) :
    IsAEKolmogorovProcess Y P p q M :=
  by
  refine ⟨hX.mk X, hX.IsKolmogorovProcess_mk, fun t ↦ ?_⟩
  filter_upwards [hX.ae_eq_mk t, h t] with ω hX hY using hY.symm.trans hX

Похожие утверждения