csinh

Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

URI: https://scilib.ai/kg/mathlib#Measurable.csinh

English

If f is measurable, then x ↦ sinh(f(x)) is measurable.

Русский

Пусть f измерима; тогда x ↦ sinh(f(x)) измерима.

LaTeX

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

Lean4

@[measurability, fun_prop]
protected theorem csinh : Measurable fun x => Complex.sinh (f x) :=
  Complex.measurable_sinh.comp hf

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

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

Разделы

Аффилиация

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