toENNRealVectorMeasure_apply_measurable

English

If i is measurable, then the i-th component of the toENNRealVectorMeasure equals the i-th measure value.

Русский

Если i измеримо, то i-я компонента toENNRealVectorMeasure равна i-му значению меры.

LaTeX

$$$\text{toENNRealVectorMeasure on measurable } i: v(i) = \mu(i)$$$

Lean4

theorem toENNRealVectorMeasure_apply_measurable {μ : Measure α} {i : Set α} (hi : MeasurableSet i) :
    μ.toENNRealVectorMeasure i = μ i :=
  if_pos hi

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