comp_snd — Mathlib

English

If f is strongly measurable, then the function z ↦ f(z.2) is strongly measurable on α×β.

Русский

Если f сильно измерима, то z ↦ f(z.2) на α×β сильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \text{StronglyMeasurable}(z \mapsto f(z.2))$$$

Lean4

protected theorem comp_snd [mα : MeasurableSpace α] {_ : MeasurableSpace β} [TopologicalSpace γ] {f : β → γ}
    (hf : StronglyMeasurable f) : StronglyMeasurable (fun z : α × β => f z.2) :=
  hf.comp_measurable measurable_snd

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