sin_arcsin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

For all x with -1 ≤ x ≤ 1, sin(arcsin x) = x.

Русский

Для всех x с -1 ≤ x ≤ 1 выполняется sin(arcsin x) = x.

LaTeX

$$$\\sin(\\arcsin x) = x \\text{ for } -1 \\le x \\le 1$$$

Lean4

theorem sin_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : sin (arcsin x) = x :=
  sin_arcsin' ⟨hx₁, hx₂⟩

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

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

Разделы

Аффилиация

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