angle_triangle

Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

URI: https://scilib.ai/kg/mathlib#InnerProductGeometry.angle_triangle

English

The angle between -x and x is π for any nonzero x.

Русский

Угол между -x и x равен π для любого ненулевого x.

LaTeX

$$$\\\\angle (-x) x = \\\\pi$ при $x \\neq 0$$$

Lean4

axiom angle_triangle (x y z : V) : angle x z ≤ angle x y + angle y z

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

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

Разделы

Аффилиация

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