measurable_betaPDFReal — Mathlib

English

For all real α, β, the function betaPDFReal α β is measurable.

Русский

Для любых действительных параметров α, β функция betaPDFReal α β измерима.

LaTeX

$$$\text{Measurable}(\betaPDFReal(\alpha,\beta))$$$

Lean4

/-- The beta pdf is measurable. -/
@[fun_prop, measurability]
theorem measurable_betaPDFReal (α β : ℝ) : Measurable (betaPDFReal α β) :=
  Measurable.ite measurableSet_Ioo (by fun_prop) (by fun_prop)

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