sub_apply

Mathlib.MeasureTheory.VectorMeasure.Basic

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

English

For any vector measures v,w and set i, (v - w)(i) = v(i) - w(i).

Русский

Для любых векторных мер v, w и множества i выполняется (v - w)(i) = v(i) - w(i).

LaTeX

$$$ (v - w)\ i = v\ i - w\ i $$$

Lean4

theorem sub_apply (v w : VectorMeasure α M) (i : Set α) : (v - w) i = v i - w i :=
  rfl

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

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

Разделы

Аффилиация

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