stieltjesOfMeasurableRat_le_one

Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.stieltjesOfMeasurableRat_le_one

← MathLib Explorer

English

For all a and x ∈ ℝ, stieltjesOfMeasurableRat f hf a x ≤ 1.

Русский

Для всех a и x ∈ ℝ, stieltjesOfMeasurableRat f hf a x ≤ 1.

LaTeX

$$$\forall a \in \alpha, \forall x \in \mathbb{R},\; stieltjesOfMeasurableRat(f,hf,a)(x) \le 1$$$

Lean4

theorem stieltjesOfMeasurableRat_le_one (hf : Measurable f) (a : α) (x : ℝ) : stieltjesOfMeasurableRat f hf a x ≤ 1 :=
  IsMeasurableRatCDF.stieltjesFunction_le_one _ a x

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

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

Разделы

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

Аффилиация

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