cos_one_le

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

Cosine at 1 is bounded above by 5/9.

Русский

Косинус в точке 1 не превышает 5/9.

LaTeX

$$$\\\\cos 1 \\\\le \\\\frac{5}{9}$$$

Lean4

theorem cos_one_le : cos 1 ≤ 5 / 9 :=
  calc
    cos 1 ≤ |(1 : ℝ)| ^ 4 * (5 / 96) + (1 - 1 ^ 2 / 2) := sub_le_iff_le_add.1 (abs_sub_le_iff.1 (cos_bound (by simp))).1
    _ ≤ 5 / 9 := by norm_num

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

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

Разделы

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

Аффилиация

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