ennrealToMeasure_apply — Mathlib

English

For measurable s, the ennrealToMeasure applied to a vector measure equals its value on s.

Русский

Для измеримого множества s выполнение ennrealToMeasure v s равно v s.

LaTeX

$$$ennrealToMeasure\ v\ s = v\ s$ for measurable s$$

Lean4

theorem ennrealToMeasure_apply {m : MeasurableSpace α} {v : VectorMeasure α ℝ≥0∞} {s : Set α} (hs : MeasurableSet s) :
    ennrealToMeasure v s = v s := by rw [ennrealToMeasure, ofMeasurable_apply _ hs]

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