neg_pi_div_two_le_arcsin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

For every real x, arcsin(x) ≥ −π/2.

Русский

Для каждого действительного x выполняется arcsin(x) ≥ −π/2.

LaTeX

$$$\\arcsin x \\ge -\\frac{\\pi}{2}$$$

Lean4

theorem neg_pi_div_two_le_arcsin (x : ℝ) : -(π / 2) ≤ arcsin x :=
  (arcsin_mem_Icc x).1

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

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

Разделы

Аффилиация

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