cos_abs

Mathlib.Analysis.Complex.Trigonometric

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

English

cos(|x|) = cos x for all real x.

Русский

cos(|x|) = cos x для всех вещественных x.

LaTeX

$$$ \cos(|x|) = \cos x $$$

Lean4

@[simp]
theorem cos_abs : cos |x| = cos x := by cases le_total x 0 <;> simp only [*, abs_of_nonneg, abs_of_nonpos, cos_neg]

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

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

Разделы

Аффилиация

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