mutuallySingular_singularPart — Mathlib

English

The singular part μ.singularPart ν is mutually singular with ν.

Русский

Сингулярная часть μ.singularPart ν взаимно сингулярна с ν.

LaTeX

$$μ.singularPart ν ⟂ₘ ν$$

Lean4

theorem mutuallySingular_singularPart (μ ν : Measure α) : μ.singularPart ν ⟂ₘ ν :=
  by
  by_cases h : HaveLebesgueDecomposition μ ν
  · exact (haveLebesgueDecomposition_spec μ ν).2.1
  · rw [singularPart_of_not_haveLebesgueDecomposition h]
    exact MutuallySingular.zero_left

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