cos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.cos

English

The cosine of a Real.Angle is defined as the lift of θ under the periodic cosine.

Русский

Косинус угла Real.Angle определяется как подъём угла через периодическую косинусоиду.

LaTeX

$$$\cos(\theta) = \cos_{\text{periodic}}(\theta)$$$

Lean4

/-- The cosine of a `Real.Angle`. -/
def cos (θ : Angle) : ℝ :=
  cos_periodic.lift θ

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

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

Разделы

Аффилиация

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