angle_nonneg

Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

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

English

For any vectors x and y, the angle between them is nonnegative.

Русский

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

LaTeX

$$$0 \\le \\\\angle x y$$$

Lean4

/-- The angle between two vectors is nonnegative. -/
theorem angle_nonneg (x y : V) : 0 ≤ angle x y :=
  Real.arccos_nonneg _

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

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

Разделы

Аффилиация

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