toSignedMeasure_zero

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

URI: https://scilib.ai/kg/mathlib#MeasureTheory.JordanDecomposition.toSignedMeasure_zero

← MathLib Explorer

English

The zero decomposition maps to the zero signed measure.

Русский

Нулевая декомпозиция переходит к нулевой сигнальной мере.

LaTeX

$$$\bigl(0: JorD\bigr).toSignedMeasure = 0$$$

Lean4

theorem toSignedMeasure_zero : (0 : JordanDecomposition α).toSignedMeasure = 0 :=
  by
  ext1 i hi
  rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self, VectorMeasure.coe_zero,
    Pi.zero_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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