measurable_right — Mathlib

English

For hf : IsRatCondKernelCDFAux f κ ν, and any a ∈ α, q ∈ ℚ, the map t ↦ f(a,t) q is measurable (in t).

Русский

Для hf: IsRatCondKernelCDFAux f κ ν и любых a ∈ α, q ∈ ℚ отображение t ↦ f(a,t) q измеримо (по t).

LaTeX

$$$\forall a\in\α, \forall q\in\mathbb{Q},\; \text{Measurable}(t\mapsto f(a,t) q).$$$

Lean4

theorem measurable_right (hf : IsRatCondKernelCDFAux f κ ν) (a : α) (q : ℚ) : Measurable (fun t ↦ f (a, t) q) :=
  by
  let h := hf.measurable
  rw [measurable_pi_iff] at h
  exact (h q).comp measurable_prodMk_left

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