angle_le_pi

Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

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

English

For any vectors x and y, the angle between them is at most π.

Русский

Для любых векторов x и y угол между ними не превосходит π.

LaTeX

$$$\\\\angle x y \\le \\\\pi$$$

Lean4

/-- The angle between two vectors is at most π. -/
theorem angle_le_pi (x y : V) : angle x y ≤ π :=
  Real.arccos_le_pi _

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

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

Разделы

Аффилиация

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