neg_ne_self_iff

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.neg_ne_self_iff

English

An angle is not equal to its negation precisely when it is not 0 or π.

Русский

Угол не равен своему отрицанию точно тогда, когда он не равен нулю и не равен π.

LaTeX

$$$ -\theta \neq \theta \iff \theta \neq 0 \\land \\theta \neq \pi. $$$

Lean4

theorem neg_ne_self_iff {θ : Angle} : -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ π := by rw [← not_or, ← neg_eq_self_iff.not]

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

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

Разделы

Аффилиация

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