not_measurable

Mathlib.MeasureTheory.VectorMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.VectorMeasure.not_measurable

English

If a set is not measurable, then the vector measure evaluates to zero on that set.

Русский

Если множество не измеримо, векторная мера принимает нулевое значение на этом множестве.

LaTeX

$$$$\\text{Not measurable}(i) \\Rightarrow v(i)=0.$$$$

Lean4

theorem not_measurable (v : VectorMeasure α M) {i : Set α} (hi : ¬MeasurableSet i) : v i = 0 :=
  v.not_measurable' hi

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru