measurable_rnDerivAux_right — Mathlib

English

The function a ↦ (x ↦ rnDerivAux κ η a x) is measurable; this is a secondary statement ensuring regularity in a.

Русский

Функция a ↦ (x ↦ rnDerivAux κ η a x) измерима; обеспечиваем регулярность по a.

LaTeX

$$$$ Measurable\_ (λ a, rnDerivAux κ η a ·) $$$$

Lean4

@[fun_prop]
theorem measurable_rnDerivAux_right (κ η : Kernel α γ) (a : α) : Measurable (fun x : γ ↦ rnDerivAux κ η a x) := by
  fun_prop

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