cos_le_one_div_sqrt_sq_add_one

Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

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

← MathLib Explorer

English

If |x| ≤ π then cos x ≤ 1/√(x^2+1).

Русский

Если |x| ≤ π, то cos x ≤ 1/√(x^2+1).

LaTeX

$$$|x| \le \pi \Rightarrow \cos x \le \dfrac{1}{\sqrt{x^2 + 1}}$$$

Lean4

theorem cos_le_one_div_sqrt_sq_add_one {x : ℝ} (hx1 : -(3 * π / 2) ≤ x) (hx2 : x ≤ 3 * π / 2) :
    cos x ≤ (1 : ℝ) / √(x ^ 2 + 1) := by
  rcases eq_or_ne x 0 with (rfl | hx3)
  · simp
  · exact (cos_lt_one_div_sqrt_sq_add_one hx1 hx2 hx3).le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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