toMeasureOfLEZero_finite — Mathlib

English

If s ≤[i] 0 and i is measurable, then s.toMeasureOfLEZero is finite.

Русский

Если s ≤[i] 0 и i измеримо, то s.toMeasureOfLEZero конечна.

LaTeX

$$$ hs : s \\le[ i ] 0 \\ \\& \\ hi : MeasurableSet i \\Rightarrow IsFiniteMeasure (s.toMeasureOfLEZero i hi) $$$

Lean4

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

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