arcsin_eq_pi_div_two

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

← MathLib Explorer

English

arcsin x = π/2 iff 1 ≤ x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem arcsin_eq_pi_div_two {x : ℝ} : arcsin x = π / 2 ↔ 1 ≤ x :=
  ⟨fun h => not_lt.1 fun h' => (arcsin_lt_pi_div_two.2 h').ne h, arcsin_of_one_le⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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