arccos_le_pi_div_four

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

← MathLib Explorer

English

For all x, arccos x ≤ π/4 iff √2/2 ≤ x.

Русский

Пусть x ∈ ℝ. Тогда arccos x ≤ π/4 тогда и только тогда, когда \sqrt{2}/2 ≤ x.

LaTeX

$$\arccos x \le \frac{\pi}{4} \iff \frac{\sqrt{2}}{2} \le x$$

Lean4

@[simp]
theorem arccos_le_pi_div_four {x} : arccos x ≤ π / 4 ↔ √2 / 2 ≤ x :=
  by
  rw [arccos, ← pi_div_four_le_arcsin]
  constructor <;>
    · intro
      linarith

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

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

Разделы

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

Аффилиация

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