eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero

English

If two unoriented angles are equal and the signs of the corresponding oriented angles are equal, then the oriented angles are equal.

Русский

Если неориентированные углы равны и знаки соответствующих ориентированных углов равны, то сами ориентированные углы равны.

LaTeX

$$$ ( \angle w x = \angle y z ) \land ( (o.oangle w x).sign = (o.oangle y z).sign ) \Rightarrow o.oangle w x = o.oangle y z $$$

Lean4

/-- If the sign of the oriented angle between two vectors is zero, either one of the vectors is
zero or the unoriented angle is 0 or π. -/
theorem eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {x y : V} (h : (o.oangle x y).sign = 0) :
    x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π :=
  by
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  rw [o.angle_eq_abs_oangle_toReal hx hy]
  rw [Real.Angle.sign_eq_zero_iff] at h
  rcases h with (h | h) <;> simp [h, Real.pi_pos.le]

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