sinc_apply

Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

URI: https://scilib.ai/kg/mathlib#Real.sinc_apply

English

For all x, sinc x equals 1 if x = 0, otherwise sin x / x.

Русский

Для любого x: sinc x равна 1, если x = 0, иначе sin x / x.

LaTeX

$$$\\operatorname{sinc}(x) = \begin{cases}1, & x=0 \\[2mm] \frac{\\sin x}{x}, & x\neq 0\end{cases}$$$

Lean4

theorem sinc_apply : sinc x = if x = 0 then 1 else sin x / x :=
  rfl

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

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

Разделы

Аффилиация

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