IicSnd_le_fst

Mathlib.Probability.Kernel.Disintegration.CondCDF

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

English

IicSnd r is absolutely continuous with respect to fst in the measure order.

Русский

IicSnd r абсолютно непрерывна по отношению к fst.

LaTeX

$$$IicSnd(r) \leqfst\ ρ$$$

Lean4

theorem IicSnd_le_fst (r : ℝ) : ρ.IicSnd r ≤ ρ.fst :=
  fst_mono restrict_le_self

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

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

Разделы

Аффилиация

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