sin

Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

URI: https://scilib.ai/kg/mathlib#AEMeasurable.sin

English

If f is AEMeasurable, then x ↦ sin(f(x)) is AEMeasurable.

Русский

Если f является AEMeasurable, то x ↦ sin(f(x)) является AEMeasurable.

LaTeX

$$$\\\\operatorname{AEMeasurable}(f)\\\\Rightarrow \\\\operatorname{AEMeasurable}(\\\\lambda x. \\\\sin(f(x)))$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru