iIndepFun_congr — Mathlib

English

If f_i and g_i are equal almost everywhere for all i, then iIndepFun f μ is equivalent to iIndepFun g μ.

Русский

Если для всех i функции f_i и g_i равны почти везде, то iIndepFun f μ эквивалентна iIndepFun g μ.

LaTeX

$$$(\forall i, f_i =^{a.e.}_{μ} g_i) \Rightarrow iIndepFun f μ \iff iIndepFun g μ$$$

Lean4

theorem iIndepFun_congr {β : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)} {f g : Π i, Ω → β i}
    (h : ∀ i, f i =ᵐ[μ] g i) : iIndepFun f μ ↔ iIndepFun g μ :=
  Kernel.iIndepFun_congr' (by simp [h])

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