arcsin_nonpos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

0 ≤ arcsin x if and only if 0 ≤ x.

Русский

0 ≤ arcsin x тогда и только тогда, когда 0 ≤ x.

LaTeX

$$$\forall x\in\mathbb{R},\ 0 \le \arcsin x \iff 0 \le x$$$

Lean4

@[simp]
theorem arcsin_nonpos {x : ℝ} : arcsin x ≤ 0 ↔ x ≤ 0 :=
  neg_nonneg.symm.trans <| arcsin_neg x ▸ arcsin_nonneg.trans neg_nonneg

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

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

Разделы

Аффилиация

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