toMeasureOfZeroLE_finite — Mathlib

English

The negation operation preserves mutual singularity relative to the full univ set: toMeasureOfLEZero_toSignedMeasure expresses equality with -s.

Русский

Отрицание сохраняет взаимную обособленность относительно всего универсума; toMeasureOfLEZero_toSignedMeasure задаёт равенство с -s.

LaTeX

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

Lean4

/-- `SignedMeasure.toMeasureOfZeroLE` is a finite measure. -/
instance toMeasureOfZeroLE_finite (hi : 0 ≤[i] s) (hi₁ : MeasurableSet i) :
    IsFiniteMeasure (s.toMeasureOfZeroLE i hi₁ hi) where
  measure_univ_lt_top := by
    rw [toMeasureOfZeroLE_apply s hi hi₁ MeasurableSet.univ]
    exact ENNReal.coe_lt_top

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