arccos_lt_arccos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

← MathLib Explorer

English

For x,y ∈ [-1,1], arccos x = arccos y if and only if x = y.

Русский

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

LaTeX

$$-1 ≤ x ≤ 1 ∧ -1 ≤ y ≤ 1 ⇒ (\arccos x = \arccos y \iff x = y)$$

Lean4

@[gcongr]
theorem arccos_lt_arccos {x y : ℝ} (hx : -1 ≤ x) (hlt : x < y) (hy : y ≤ 1) : arccos y < arccos x := by unfold arccos;
  gcongr <;> assumption

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

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

Разделы

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

Аффилиация

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