IicSnd

Mathlib.Probability.Kernel.Disintegration.CondCDF

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

English

If ρ is finite, then IicSnd r is finite for every r.

Русский

Если ρ конечна, то IicSnd r конечна для любого r.

LaTeX

$$$[\text{IsFiniteMeasure}(\rho)]\Rightarrow \text{IsFiniteMeasure}(\rho.IicSnd r)$$$

Lean4

theorem IicSnd {ρ : Measure (α × ℝ)} [IsFiniteMeasure ρ] (r : ℝ) : IsFiniteMeasure (ρ.IicSnd r) :=
  isFiniteMeasure_of_le _ (IicSnd_le_fst ρ _)

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

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

Разделы

Аффилиация

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