sin_angle_nonneg

Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$0 \\le \\sin(\\\\angle x y)$$$

Lean4

/-- The sine of the angle between two vectors is nonnegative. -/
theorem sin_angle_nonneg (x y : V) : 0 ≤ sin (angle x y) :=
  sin_nonneg_of_nonneg_of_le_pi (angle_nonneg x y) (angle_le_pi x y)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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