singularPart_sub — Mathlib

English

Let s and t be signed measures with Lebesgue decomposition with respect to μ. Then the singular part of s − t equals the singular part of s minus the singular part of t.

Русский

Пусть s и t — знаковые мeры, имеющие разложение Лебега по отношению к μ. Тогда сингулярная часть s − t равна сингулярной части s минус сингулярная часть t.

LaTeX

$$$ (s - t).singularPart \\mu = s.singularPart \\mu - t.singularPart \\mu $$$

Lean4

theorem singularPart_sub (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
    [t.HaveLebesgueDecomposition μ] : (s - t).singularPart μ = s.singularPart μ - t.singularPart μ := by
  rw [sub_eq_add_neg, sub_eq_add_neg, singularPart_add, singularPart_neg]

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