oangle_sub_eq_oangle_sub_rev_of_norm_eq

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

URI: https://scilib.ai/kg/mathlib#Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq

← MathLib Explorer

English

If ‖x‖ = ‖y‖, then o.oangle x (x - y) = o.oangle (y - x) y.

Русский

Если ‖x‖ = ‖y‖, то o.oangle x (x - y) = o.oangle (y - x) y.

LaTeX

$$$o.oangle x (x - y) = o.oangle (y - x) y \text{ при } \|x\| = \|y\|$$$

Lean4

/-- Pons asinorum, oriented vector angle form. -/
theorem oangle_sub_eq_oangle_sub_rev_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖) : o.oangle x (x - y) = o.oangle (y - x) y :=
  by simp [oangle, h]

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

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

Разделы

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

Аффилиация

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