sinc

Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc

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

English

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

Русский

Если f измерима, то x ↦ sinc(f(x)) измерима.

LaTeX

$$$ \\text{Measurable}(f) \\Rightarrow \\text{Measurable}(\\lambda x, \\text{Real}.sinc(f(x))) $$$

Lean4

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

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

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

Разделы

Аффилиация

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