sinOrderIso — Mathlib

English

The sine function restricted to [-π/2, π/2] is an order isomorphism onto [-1,1].

Русский

Ограничение функции синус на [-π/2, π/2] является упорядоченным биективным отображением на [-1,1].

LaTeX

$$$\\\\sin|_{[-\\\\frac{\\\\pi}{2}, \\\\frac{\\\\pi}{2}]} : [-\\\\frac{\\\\pi}{2}, \\\\frac{\\\\pi}{2}] \\\\to [-1,1] \\\\simeq_o [-1,1]$$$

Lean4

/-- `Real.sin` as an `OrderIso` between `[-(π / 2), π / 2]` and `[-1, 1]`. -/
def sinOrderIso : Icc (-(π / 2)) (π / 2) ≃o Icc (-1 : ℝ) 1 :=
  (strictMonoOn_sin.orderIso _ _).trans <| OrderIso.setCongr _ _ bijOn_sin.image_eq

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