prod_swap — Mathlib

English

If f is strongly measurable on α×β → γ, then f with swapped arguments is strongly measurable.

Русский

Если f сильно измерима на α×β → γ, то f, где аргументы поменяны местами, тоже сильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \text{StronglyMeasurable}(x \mapsto f(x.swap))$$$

Lean4

protected theorem prod_swap {_ : MeasurableSpace α} {_ : MeasurableSpace β} [TopologicalSpace γ] {f : β × α → γ}
    (hf : StronglyMeasurable f) : StronglyMeasurable (fun z : α × β => f z.swap) :=
  hf.comp_measurable measurable_swap

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