toMeasureOfLEZero — Mathlib

English

The measure obtained from s.toMeasureOfZeroLE is finite on the universal set.

Русский

Мера, полученная из s.toMeasureOfZeroLE, конечна на все пространство.

LaTeX

$$$ IsFiniteMeasure\\ (s.toMeasureOfZeroLE\\ Set.univ) $$$

Lean4

/-- Given a signed measure `s` and a negative measurable set `i`, `toMeasureOfLEZero`
provides the measure, mapping measurable sets `j` to `-s (i ∩ j)`. -/
def toMeasureOfLEZero (s : SignedMeasure α) (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : s ≤[i] 0) : Measure α :=
  toMeasureOfZeroLE (-s) i hi₁ <| @neg_zero (VectorMeasure α ℝ) _ ▸ neg_le_neg _ _ hi₁ hi₂

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