angle_nonneg

Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

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

English

The angle at any triple of points is nonnegative: 0 ≤ ∠ p1 p2 p3.

Русский

Угол при любой тройке точек неотрицателен: 0 ≤ ∠ p1 p2 p3.

LaTeX

$$$0 \le \angle p_1 p_2 p_3$$$

Lean4

/-- The angle at a point is nonnegative. -/
nonrec theorem angle_nonneg (p₁ p₂ p₃ : P) : 0 ≤ ∠ p₁ p₂ p₃ :=
  angle_nonneg _ _

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

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

Разделы

Аффилиация

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