sinc_le_one

Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

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

English

The sinc function is bounded above by 1: sinc x ≤ 1 for all x.

Русский

Функция sinc ограничена сверху единицей: sinc x ≤ 1 для всех x.

LaTeX

$$$\operatorname{sinc} x \le 1$$$

Lean4

theorem sinc_le_one (x : ℝ) : sinc x ≤ 1 :=
  (abs_le.mp (abs_sinc_le_one x)).2

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

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

Разделы

Аффилиация

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