IicSnd_mono

Mathlib.Probability.Kernel.Disintegration.CondCDF

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

English

If r ≤ r', then ρ.IicSnd r ≤ ρ.IicSnd r'.

Русский

Если r ≤ r', то ρ.IicSnd r ≤ ρ.IicSnd r'.

LaTeX

$$$\forall \; r \le r',\; ρ.IicSnd r \leq ρ.IicSnd r'$$$

Lean4

@[gcongr]
theorem IicSnd_mono {r r' : ℝ} (h_le : r ≤ r') : ρ.IicSnd r ≤ ρ.IicSnd r' := by unfold IicSnd; gcongr

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

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

Разделы

Аффилиация

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