sign — Mathlib

English

For any angle θ, the sign of θ equals the sign of sin θ.

Русский

Для любого угла θ знак θ равно знаку синуса θ.

LaTeX

$$$ \operatorname{sign}(\theta) = \operatorname{sign}(\sin \theta) $$$

Lean4

/-- The sign of a `Real.Angle` is `0` if the angle is `0` or `π`, `1` if the angle is strictly
between `0` and `π` and `-1` is the angle is strictly between `-π` and `0`. It is defined as the
sign of the sine of the angle. -/
def sign (θ : Angle) : SignType :=
  SignType.sign (sin θ)

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