sinc — Mathlib

English

If f is almost everywhere measurable, then x ↦ sinc(f(x)) is almost everywhere measurable.

Русский

Если f измерима почти всюду, то x ↦ sinc(f(x)) измерима почти всюду.

LaTeX

$$$ (AEMeasurable\\ f\\ μ) \\rightarrow AEMeasurable\\ (\\lambda x, \\text{Real}.sinc(f(x)))\\ μ $$$

Lean4

@[fun_prop, measurability]
protected theorem sinc (hf : AEMeasurable f μ) : AEMeasurable (fun x ↦ sinc (f x)) μ :=
  Real.measurable_sinc.comp_aemeasurable hf

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