arcsin_mem_Icc

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

Let x be a real number. Then arcsin(x) lies in the closed interval [−π/2, π/2].

Русский

Пусть x — действительное число. Тогда arcsin(x) принадлежит отрезку [−π/2, π/2].

LaTeX

$$$\\arcsin x \\in \\left[-\\frac{\\pi}{2}, \\frac{\\pi}{2}\\right]$$$

Lean4

theorem arcsin_mem_Icc (x : ℝ) : arcsin x ∈ Icc (-(π / 2)) (π / 2) :=
  Subtype.coe_prop _

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

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

Разделы

Аффилиация

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