sinc_le_inv_abs

Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

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

English

For all x ≠ 0, sinc x ≤ |x|^{-1}.

Русский

Для всех x ≠ 0 выполняется sinc x ≤ |x|^{-1}.

LaTeX

$$$x \neq 0 \Rightarrow \operatorname{sinc} x \le |x|^{-1}$$$

Lean4

theorem sinc_le_inv_abs (hx : x ≠ 0) : sinc x ≤ |x|⁻¹ :=
  by
  rw [sinc_of_ne_zero hx]
  exact sin_div_le_inv_abs x

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

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

Разделы

Аффилиация

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