arccos_eq_of_eq_cos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

If 0 ≤ y ≤ π and x = cos y, then arccos x = y.

Русский

Пусть y ∈ [0, π] и x = cos y, тогда arccos x = y.

LaTeX

$$0 \le y \le \pi \land x = \cos y \Rightarrow \arccos x = y$$

Lean4

theorem arccos_eq_of_eq_cos (hy₀ : 0 ≤ y) (hy₁ : y ≤ π) (hxy : x = cos y) : arccos x = y := by
  rw [hxy, arccos_cos hy₀ hy₁]

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

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

Разделы

Аффилиация

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