neg_pi_div_two_eq_arcsin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

-π/2 = arcsin x iff x ≤ −1.

Русский

-π/2 = arcsin x тогда и только тогда, когда x ≤ −1.

LaTeX

$$$-\frac{\pi}{2} = \arcsin x \iff x \le -1$$$

Lean4

@[simp]
theorem neg_pi_div_two_eq_arcsin {x} : -(π / 2) = arcsin x ↔ x ≤ -1 :=
  eq_comm.trans arcsin_eq_neg_pi_div_two

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

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

Разделы

Аффилиация

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