fst — Mathlib

English

If f is AEMeasurable into a product β×γ, then its first coordinate function x ↦ (f x)1 is AEMeasurable.

Русский

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

LaTeX

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

Lean4

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

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