restrict_le_zero_of_not_measurable

English

Let i be a subset of α which is not measurable. Then the vector measure v restricted to i is bounded above by the zero vector measure on i; in particular, (v restricted to i) ≤ 0.

Русский

Пусть i — подмножество множества α, не измеримое. Тогда векторная мера v, ограниченная на i, не превышает нулевую векторную меру на i; то есть v|_i ≤ 0.

LaTeX

$$$v\restriction i \le 0$$$

Lean4

theorem restrict_le_zero_of_not_measurable (hi : ¬MeasurableSet i) : v ≤[i] 0 := by
  rw [restrict_zero, restrict_not_measurable _ hi]

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