nonneg_of_zero_le_restrict

Mathlib.MeasureTheory.VectorMeasure.Basic

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

← MathLib Explorer

English

If 0 ≤[i] v, then 0 ≤ v i.

Русский

Если 0 ≤[i] v, то 0 ≤ v i.

LaTeX

$$$ 0 \\le\\,[i] v \\Rightarrow 0 \\le v(i) $$$

Lean4

theorem nonneg_of_zero_le_restrict (hi₂ : 0 ≤[i] v) : 0 ≤ v i :=
  by
  by_cases hi₁ : MeasurableSet i
  · exact (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl
  · rw [v.not_measurable hi₁]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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