right_ne_zero_of_oangle_ne_zero — Mathlib

English

If p3 and p4 lie on opposite sides of s, the signs are opposite: (∡p1 p4 p2).sign = - (∡p1 p3 p2).sign.

Русский

Если p3 и p4 лежат по противоположным сторонам от s, знаки углов противоположны.

LaTeX

$$$(\angle p_1 p_4 p_2).\sign = - (\angle p_1 p_3 p_2).\sign$$$

Lean4

/-- If the angle between two vectors is nonzero, the second vector is nonzero. -/
theorem right_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : y ≠ 0 := by rintro rfl; simp at h

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