iIndepFun_congr' — Mathlib

English

If f_i and g_i are a.e.-equal for κ a for all i, then iIndepFun f κ μ iff iIndepFun g κ μ.

Русский

Если для каждого i функции f_i и g_i совпадают почти наверняка по мере κ a, то iIndepFun f κ μ эквивалентно iIndepFun g κ μ.

LaTeX

$$$iIndepFun f κ μ \Rightarrow iIndepFun g κ μ$ whenever f_i =ᵐ[κ a] g_i a.e.$$

Lean4

theorem iIndepFun_congr' {β : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)} {f g : Π i, Ω → β i}
    (h : ∀ i, ∀ᵐ a ∂μ, f i =ᵐ[κ a] g i) : iIndepFun f κ μ ↔ iIndepFun g κ μ
    where
  mp h' := h'.congr' h
  mpr
    h' := by
    refine h'.congr' fun i ↦ ?_
    filter_upwards [h i] with a ha using ha.symm

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