snd — Mathlib

English

If f is AEMeasurable into β×γ, then its second coordinate function x ↦ (f x)2 is AEMeasurable.

Русский

Если f — AЕ-измеримая функция в β×γ, то вторая координата f2(x) = (f(x)).2 также AЕ-измерима.

LaTeX

$$$\mathrm{AEMeasurable}(f, \mu) \rightarrow \mathrm{AEMeasurable}(\lambda x. (f x)_{2}, \mu)$$$

Lean4

@[fun_prop, measurability]
protected theorem snd {f : α → β × γ} (hf : AEMeasurable f μ) : AEMeasurable (fun x ↦ (f x).2) μ :=
  measurable_snd.comp_aemeasurable hf

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