cos_arcsin_nonneg

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

← MathLib Explorer

English

For every real x, cos(arcsin x) ≥ 0.

Русский

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

LaTeX

$$$\forall x\in\mathbb{R},\ 0 \le \cos(\arcsin x)$$$

Lean4

theorem cos_arcsin_nonneg (x : ℝ) : 0 ≤ cos (arcsin x) :=
  cos_nonneg_of_mem_Icc
    ⟨neg_pi_div_two_le_arcsin _, arcsin_le_pi_div_two _⟩
      -- The junk values for `arcsin` and `sqrt` make this true even outside `[-1, 1]`.

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

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

Разделы

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

Аффилиация

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