bijOn_sin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#Real.bijOn_sin

English

The sine function restricted to [-π/2, π/2] is a bijection onto [-1,1].

Русский

Синус на отрезке [-π/2, π/2] является биекцией с [-1,1].

LaTeX

$$$\text{BijOn}(\sin, [-\\frac{\\pi}{2},\\frac{\\pi}{2}], [-1,1]).$$$

Lean4

theorem bijOn_sin : BijOn sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1) :=
  ⟨mapsTo_sin _, injOn_sin, surjOn_sin⟩

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

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

Разделы

Аффилиация

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