ae_ae_eq_of_ae_eq_uncurry — Mathlib

English

If the uncurried forms uncurry f and uncurry g are almost everywhere equal with respect to μ × ν, then for μ-almost every x the functions f x and g x are ν-almost everywhere equal.

Русский

Если неконкурированные формы uncurry f и uncurry g равны почти наверняка относительно μ × ν, то для почти всех x по μ функции f x и g x равны почти наверняка по ν.

LaTeX

$$$(uncurry\; f =^{\mathrm{a.e.}}_{μ \otimes ν} uncurry\; g) \Rightarrow ∀^{\!} x \partial μ, curry\; f\; x =^{\mathrm{a.e.}}_{ν} curry\; g\; x$$$

Lean4

theorem ae_ae_eq_of_ae_eq_uncurry {γ : Type*} {f g : α → β → γ} (h : uncurry f =ᵐ[μ.prod ν] uncurry g) :
    ∀ᵐ x ∂μ, f x =ᵐ[ν] g x :=
  ae_ae_eq_curry_of_prod h

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