arctan_eq_neg_pi_div_four

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

arctan x equals -π/4 if and only if x equals -1.

Русский

arctan x = -π/4 тогда и только тогда, когда x = -1.

LaTeX

$$$\\arctan x = -\\frac{\\pi}{4} \\iff x = -1$$$

Lean4

@[simp]
theorem arctan_eq_neg_pi_div_four : arctan x = -(π / 4) ↔ x = -1 :=
  arctan_injective.eq_iff' <| by rw [arctan_neg, arctan_one]

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

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

Разделы

Аффилиация

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