compProd_of_right' — Mathlib

English

If κ a ⟂ η a for ν-almost every a, and κ, η are finite kernels, then μ ⊗ₘ κ ⟂ ν ⊗ₘ η (the symmetric version of compProd_of_right).

Русский

Если κ(a) и η(a) взаимно параллельны ν-почти для почти всех a, тогда μ ⊗ₘ κ ⟂ ν ⊗ₘ η (симметрическая версия compProd_of_right).

LaTeX

$$$\\bigl(\\forall^{\\text{ae}} a \\partial ν, κ(a) \\perp_m η(a)\\bigr) \\Rightarrow μ \\otimes_m κ \\perp_m ν \\otimes_m η.$$$

Lean4

theorem compProd_of_right' (μ ν : Measure α) (hκη : ∀ᵐ a ∂ν, κ a ⟂ₘ η a) : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η :=
  by
  refine (MutuallySingular.compProd_of_right _ _ ?_).symm
  simp_rw [MutuallySingular.comm, hκη]

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