abs_cos_le_one

Mathlib.Analysis.Complex.Trigonometric

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

English

Let x be a real number. Then |cos x| ≤ 1.

Русский

Пусть x — действительное число. Тогда |cos x| ≤ 1.

LaTeX

$$$|\\cos x| \\le 1$$$

Lean4

theorem abs_cos_le_one : |cos x| ≤ 1 :=
  abs_le_one_iff_mul_self_le_one.2 <| by simp only [← sq, cos_sq_le_one]

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

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

Разделы

Аффилиация

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