restrict_zero_set

Mathlib.MeasureTheory.Measure.Restrict

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.restrict_zero_set

English

For a set s and a null-measurable t, μ|_{s∩t} + μ|_{s\t} = μ|_s.

Русский

Для множества s и нулевой измеримости t имеем μ|_{s∩t} + μ|_{s\t} = μ|_s.

LaTeX

$$$ \mu.restrict (s \cap t) + \mu.restrict (s \setminus t) = \mu.restrict s $$$

Lean4

theorem restrict_zero_set {s : Set α} (h : μ s = 0) : μ.restrict s = 0 :=
  restrict_eq_zero.2 h

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

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

Разделы

Аффилиация

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