cos_arctan_pos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

For every x, cos(arctan x) > 0.

Русский

Для любого x: cos(arctan x) > 0.

LaTeX

$$$ 0 < \cos(\arctan x) $$$

Lean4

theorem cos_arctan_pos (x : ℝ) : 0 < cos (arctan x) :=
  cos_pos_of_mem_Ioo <| arctan_mem_Ioo x

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

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

Разделы

Аффилиация

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