arcsin_sin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

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₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) : arcsin (sin x) = x :=
  arcsin_sin' ⟨hx₁, hx₂⟩

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

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

Разделы

Аффилиация

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