arccos_inj

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

← MathLib Explorer

English

For x,y ∈ [-1,1], arccos x = arccos y implies x = y.

Русский

Для x,y ∈ [-1,1], равенство arccos x = arccos y влечёт x = y.

LaTeX

$$-1 ≤ x ≤ 1 ∧ -1 ≤ y ≤ 1 ∧ \arccos x = \arccos y \Rightarrow x = y$$

Lean4

theorem arccos_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) : arccos x = arccos y ↔ x = y :=
  arccos_injOn.eq_iff ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩

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

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

Разделы

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

Аффилиация

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