IicSnd_univ

Mathlib.Probability.Kernel.Disintegration.CondCDF

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

English

IicSnd r on univ equals ρ (univ × Iic r).

Русский

IicSnd r на унив равна ρ(унив × Iic r).

LaTeX

$$$\rho.IicSnd(r)\;\mathrm{univ} = \rho\left(\mathrm{univ} \times Iic(r)\right)$$$

Lean4

theorem IicSnd_univ (r : ℝ) : ρ.IicSnd r univ = ρ (univ ×ˢ Iic r) :=
  IicSnd_apply ρ r MeasurableSet.univ

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

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

Разделы

Аффилиация

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