measurable_of_not_zero_le_restrict

Mathlib.MeasureTheory.VectorMeasure.Basic

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

English

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

Русский

Если ограничение векторной меры v на i не менее нуля, тогда i — измеримое множество.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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