measurable_of_not_restrict_le_zero

Mathlib.MeasureTheory.VectorMeasure.Basic

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

English

If the restriction of v to i is not greater than or equal to zero, then i is measurable.

Русский

Если ограничение векторной меры v на i не больше или равно нулю, тогда i измеримо.

LaTeX

$$¬(v \le_i 0) \Rightarrow \MeasurableSet(i)$$

Lean4

theorem measurable_of_not_restrict_le_zero (hi : ¬v ≤[i] 0) : MeasurableSet i :=
  Not.imp_symm (restrict_le_zero_of_not_measurable _) hi

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

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

Разделы

Аффилиация

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