arcsin_neg_one

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

← MathLib Explorer

English

Arcsin of minus one equals −π/2.

Русский

Arcsin от −1 равен −π/2.

LaTeX

$$$\\arcsin(-1) = -\\frac{\\pi}{2}$$$

Lean4

theorem arcsin_neg_one : arcsin (-1) = -(π / 2) :=
  arcsin_eq_of_sin_eq (by rw [sin_neg, sin_pi_div_two]) <| left_mem_Icc.2 (neg_le_self pi_div_two_pos.le)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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