neg_one_le_sinc

Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

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

English

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

Русский

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

LaTeX

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

Lean4

theorem neg_one_le_sinc (x : ℝ) : -1 ≤ sinc x :=
  (abs_le.mp (abs_sinc_le_one x)).1

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

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

Разделы

Аффилиация

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