jordanDecompositionOfToSignedMeasureSub_posPart

Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_posPart

Lean4

theorem jordanDecompositionOfToSignedMeasureSub_posPart :
    (jordanDecompositionOfToSignedMeasureSub μ ν).posPart = μ - ν :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru