zero_mem_measureOfNegatives

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SignedMeasure.zero_mem_measureOfNegatives

English

0 is an element of measureOfNegatives(s) for any signed measure s.

Русский

0 принадлежит measureOfNegatives(s) для любой сигнальной меры s.

LaTeX

$$$0 \in \mathrm{measureOfNegatives}(s)$$$

Lean4

theorem zero_mem_measureOfNegatives : (0 : ℝ) ∈ s.measureOfNegatives :=
  ⟨∅, ⟨MeasurableSet.empty, le_restrict_empty _ _⟩, s.empty⟩

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

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

Разделы

Аффилиация

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