English
Two unoriented angles are equal iff the oriented angles are equal, provided the signs agree.
Русский
Угол неориентированный равен тогда и только тогда, когда ориентированные углы равны при согласованных знаках.
LaTeX
$$$ \angle w x = \angle y z \iff o.oangle w x = o.oangle y z \text{ given } (o.oangle w x).sign = (o.oangle y z).sign $$$
Lean4
/-- If two unoriented angles are equal, and the signs of the corresponding oriented angles are
equal, then the oriented angles are equal (even in degenerate cases). -/
theorem oangle_eq_of_angle_eq_of_sign_eq {w x y z : V}
(h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z)
(hs : (o.oangle w x).sign = (o.oangle y z).sign) : o.oangle w x = o.oangle y z :=
by
by_cases h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
· have hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0 :=
by
rcases h0 with ((rfl | rfl) | rfl | rfl)
· simpa using hs.symm
· simpa using hs.symm
· simpa using hs
· simpa using hs
rcases hs' with ⟨hswx, hsyz⟩
have h' : InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2 :=
by
rcases h0 with ((rfl | rfl) | rfl | rfl)
· simpa using h.symm
· simpa using h.symm
· simpa using h
· simpa using h
rcases h' with ⟨hwx, hyz⟩
have hpi : π / 2 ≠ π := by
intro hpi
rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel_right] at hpi
· exact Real.pi_pos.ne.symm hpi
· exact two_ne_zero
have h0wx : w = 0 ∨ x = 0 :=
by
have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx
simpa [hwx, Real.pi_pos.ne.symm, hpi] using h0'
have h0yz : y = 0 ∨ z = 0 :=
by
have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hsyz
simpa [hyz, Real.pi_pos.ne.symm, hpi] using h0'
rcases h0wx with (h0wx | h0wx) <;> rcases h0yz with (h0yz | h0yz) <;> simp [h0wx, h0yz]
· push_neg at h0
rw [Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq hs]
rwa [o.angle_eq_abs_oangle_toReal h0.1.1 h0.1.2, o.angle_eq_abs_oangle_toReal h0.2.1 h0.2.2] at h
