mutuallySingular_singularPart — Mathlib

English

The singular part of κ with respect to η is mutually singular with η at every a.

Русский

Сингулярная часть κ по отношению к η несовместима с η на каждом a.

LaTeX

$$$ singularPart(\kappa, \eta)(a) \perp_{m} \eta(a) $$$

Lean4

/-- The singular part of `κ` with respect to `η` is mutually singular with `η`. -/
theorem mutuallySingular_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
    singularPart κ η a ⟂ₘ η a := by
  symm
  exact
    ⟨mutuallySingularSetSlice κ η a, measurableSet_mutuallySingularSetSlice κ η a,
      measure_mutuallySingularSetSlice κ η a, singularPart_compl_mutuallySingularSetSlice κ η a⟩

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