of_uncurry_right — Mathlib

English

If the uncurry of f is strongly measurable, then for every y, the function x ↦ f(x) y is strongly measurable.

Русский

Если uncurry f сильно измерима, то для каждого y функция x ↦ f(x)(y) сильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(\text{uncurry } f) \Rightarrow \forall y,\ \text{StronglyMeasurable}(x \mapsto f(x) y)$$$

Lean4

theorem of_uncurry_right [TopologicalSpace β] {_ : MeasurableSpace α} {_ : MeasurableSpace γ} {f : α → γ → β}
    (hf : StronglyMeasurable (uncurry f)) {y : γ} : StronglyMeasurable fun x => f x y :=
  hf.comp_measurable measurable_prodMk_right

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