indepFun_congr — Mathlib

English

Let κ and η be kernels from α to Ω and μ a measure on α. If κ and η are equal μ-almost everywhere, then for any measurable functions f, g : Ω → respective targets, IndepFun f g κ μ holds if and only if IndepFun f g η μ holds.

Русский

Пусть κ и η — ядра от α к Ω, μ — мера на α. Если κ и η равны μ-почти где-либо, тогда для любых измеримых функций f, g : Ω → соответствующие цели выполняется, что IndepFun f g κ μ эквивалентно IndepFun f g η μ.

LaTeX

$$$ (κ =^{\\mathrm{ae}}_{\\mu} η) \\Rightarrow \\bigl(IndepFun\\ f\\ g\\ κ\\ μ \\iff IndepFun\\ f\\ g\\ η\\ μ\\bigr) $$$

Lean4

theorem indepFun_congr {β γ} [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ} (h : κ =ᵐ[μ] η) :
    IndepFun f g κ μ ↔ IndepFun f g η μ :=
  indep_congr h

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