toMeasureOfLEZero_toSignedMeasure

English

For hs : s ≤ Set.univ 0, the toMeasureOfLEZero_toSignedMeasure equals -s.

Русский

Для hs: s ≤ Set.univ 0, toMeasureOfLEZero_toSignedMeasure = -s.

LaTeX

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

Lean4

theorem toMeasureOfLEZero_toSignedMeasure (hs : s ≤[Set.univ] 0) :
    (s.toMeasureOfLEZero Set.univ MeasurableSet.univ hs).toSignedMeasure = -s :=
  by
  ext i hi
  simp [hi, toMeasureOfLEZero_apply _ _ _ hi, measureReal_def]

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