instCoeFun

Mathlib.MeasureTheory.VectorMeasure.Basic

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

English

If a set i is not measurable, then the vector measure of i is zero.

Русский

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

LaTeX

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

Lean4

instance instCoeFun : CoeFun (VectorMeasure α M) fun _ => Set α → M :=
  ⟨VectorMeasure.measureOf'⟩

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

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

Разделы

Аффилиация

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