sin — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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