haveLebesgueDecompositionSMul

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

← MathLib Explorer

English

For NNReal r, (r • μ).HaveLebesgueDecomposition ν.

Русский

Для NNReal r, (r • μ) имеет разложение Лебега относительно ν.

LaTeX

$$(r • μ).HaveLebesgueDecomposition ν$$

Lean4

instance haveLebesgueDecompositionSMul (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] (r : ℝ≥0) :
    (r • μ).HaveLebesgueDecomposition ν := by rw [ENNReal.smul_def]; infer_instance

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

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

Разделы

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

Аффилиация

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