toMeasureOfZeroLE_toSignedMeasure

English

There is a natural equivalence between toMeasureOfLEZero_toSignedMeasure and -s via off-sets on Set.univ.

Русский

Существует естественное эквивалентное соответствие между toMeasureOfLEZero_toSignedMeasure и -s через множители на Set.univ.

LaTeX

$$$ (\\text{toMeasureOfLEZero Set.univ MeasurableSet.univ hs).toSignedMeasure = -s $$$

Lean4

theorem toMeasureOfZeroLE_toSignedMeasure (hs : 0 ≤[Set.univ] s) :
    (s.toMeasureOfZeroLE Set.univ MeasurableSet.univ hs).toSignedMeasure = s :=
  by
  ext i hi
  simp [hi, toMeasureOfZeroLE_apply _ _ _ hi, measureReal_def]

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