arcsin_sin'

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

URI: https://scilib.ai/kg/mathlib#Real.arcsin_sin'

← MathLib Explorer

English

If x ∈ [−π/2, π/2], arcsin(sin x) = x.

Русский

Если x ∈ [−π/2, π/2], тогда arcsin(sin x) = x.

LaTeX

$$$\\arcsin(\\sin x) = x \\text{ for } x \\in [-\\frac{\\pi}{2}, \\frac{\\pi}{2}]$$$

Lean4

theorem arcsin_sin' {x : ℝ} (hx : x ∈ Icc (-(π / 2)) (π / 2)) : arcsin (sin x) = x :=
  injOn_sin (arcsin_mem_Icc _) hx <| by rw [sin_arcsin (neg_one_le_sin _) (sin_le_one _)]

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

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

Разделы

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

Аффилиация

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