sinh — Mathlib

English

Let f be almost everywhere measurable with respect to μ; then x ↦ sinh(f(x)) is almost everywhere measurable with respect to μ.

Русский

Пусть f ~почти всюду измерима относительно μ; тогда x ↦ sinh(f(x)) ~почти всюду измерима относительно μ.

LaTeX

$$$AEMeasurable\\ f\\ μ \\rightarrow AEMeasurable\\bigl(\\lambda x. \\sinh(f(x))\\bigr)\\ μ$$$

Lean4

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

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