pi_div_two_eq_arcsin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

π/2 = arcsin x iff 1 ≤ x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem pi_div_two_eq_arcsin {x} : π / 2 = arcsin x ↔ 1 ≤ x :=
  eq_comm.trans arcsin_eq_pi_div_two

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

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

Разделы

Аффилиация

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