cos — Mathlib

English

The real cosine is the real part of the complex cosine on real inputs; i.e., for x ∈ ℝ, Real.cos x = Re( Complex.cos( Complex.ofReal x ) ).

Русский

Реальный косинус есть реальная часть комплексного косинуса на вещественных входах: для x ∈ ℝ выполнено Real.cos x = Re( Complex.cos( Complex.ofReal x ) ).

LaTeX

$$$$ \operatorname{Real.cos}(x) = \operatorname{Re}\bigl( \operatorname{Complex.cos}(\operatorname{Complex.ofReal}(x))\bigr). $$$$

Lean4

/-- The real cosine function, defined as the real part of the complex cosine -/
@[pp_nodot]
nonrec def cos (x : ℝ) : ℝ :=
  (cos x).re

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