oangle_self_right

Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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

English

The oriented angle at p2 with both rays starting from p2 toward p1 equals zero when p1 equals p1.

Русский

Ориентированный угол ∡ p1 p2 p1 равен нулю, когда первая и третья точки совпадают.

LaTeX

$$$\\angle p_1 p_2 p_1 = 0$$$

Lean4

/-- The angle ∡ABB at a point. -/
@[simp]
theorem oangle_self_right (p₁ p₂ : P) : ∡ p₁ p₂ p₂ = 0 := by simp [oangle]

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

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

Разделы

Аффилиация

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