fst — Mathlib

English

If f maps α to β × γ and is AEStronglyMeasurable, then the projections (f x).1 and (f x).2 are AEStronglyMeasurable.

Русский

Если f: α→β×γ AE‑строго измерима, то проекции f1 и f2 AE‑строго измеримы.

LaTeX

$$$AEStronglyMeasurable_m(f, \\mu) \\Rightarrow AEStronglyMeasurable_m(\\lambda x. (f x).1, \\mu)$ and similarly for .2$$

Lean4

@[fun_prop]
protected theorem fst {f : α → β × γ} (hf : AEStronglyMeasurable[m] f μ) :
    AEStronglyMeasurable[m] (fun x ↦ (f x).1) μ :=
  continuous_fst.comp_aestronglyMeasurable hf

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