measurable_rnDeriv

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

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

English

The function rnDeriv s μ is measurable for any signed measure s and measure μ.

Русский

Функция rnDeriv s μ измерима для любой знаковой меры s и меры μ.

LaTeX

$$Measurable (rnDeriv s μ)$$

Lean4

@[measurability]
theorem measurable_rnDeriv (s : SignedMeasure α) (μ : Measure α) : Measurable (rnDeriv s μ) :=
  by
  rw [rnDeriv_def]
  fun_prop

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

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

Разделы

Аффилиация

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