IsMeasurableRatCDF_defaultRatCDF — Mathlib

English

The family of functions (a, q) ↦ defaultRatCDF(q) is measurable with respect to the product measurable structure on α × ℚ.

Русский

Семейство функций (a, q) ↦ defaultRatCDF(q) измеримо по произведению мерозадающих структур на α × ℚ.

LaTeX

$$$$\\text{IsMeasurableRatCDF}(\\lambda (a,q). \\mathrm{defaultRatCDF}(q)).$$$$

Lean4

theorem IsMeasurableRatCDF_defaultRatCDF (α : Type*) [MeasurableSpace α] :
    IsMeasurableRatCDF (fun (_ : α) (q : ℚ) ↦ defaultRatCDF q)
    where
  isRatStieltjesPoint := isRatStieltjesPoint_defaultRatCDF
  measurable := measurable_const

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