English
Let κ and η be kernels from α to Ω and μ a measure on α. If κ and η are equal μ-almost everywhere as kernels, then for any family of target spaces β_i and any f : ∀ i, Ω → β_i, the independence relation iIndepFun f κ μ holds if and only if iIndepFun f η μ holds.
Русский
Пусть κ и η — ядра от α в Ω, μ — мера на α. Если κ и η совпадают μ-почти где угодно как ядра, то для любой семейства пространств β_i и любого f : ∀ i, Ω → β_i справедливо, что независимость iIndepFun f κ μ эквивалентна независимости iIndepFun f η μ.
LaTeX
$$$ (\\kappa =^{\\mathrm{ae}}_{\\mu} \\eta) \\Rightarrow \\bigl(iIndepFun\\ f\\ \\kappa\\ \\mu \\iff iIndepFun\\ f\\ \\eta\\ \\mu\\bigr) $$$
Lean4
theorem iIndepFun_congr {β : ι → Type*} {m : ∀ x : ι, MeasurableSpace (β x)} {f : ∀ x : ι, Ω → β x} (h : κ =ᵐ[μ] η) :
iIndepFun f κ μ ↔ iIndepFun f η μ :=
iIndep_congr h
