angle_le_pi

Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

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

English

The angle at a point is at most π: ∠ p1 p2 p3 ≤ π.

Русский

Угол в точке не превосходит π: ∠ p1 p2 p3 ≤ π.

LaTeX

$$$\angle p_1 p_2 p_3 \le \pi$$$

Lean4

/-- The angle at a point is at most π. -/
nonrec theorem angle_le_pi (p₁ p₂ p₃ : P) : ∠ p₁ p₂ p₃ ≤ π :=
  angle_le_pi _ _

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

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

Разделы

Аффилиация

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