English
For a triangle t, t.AcuteAngled is equivalent to all three internal angles being less than π/2.
Русский
Для треугольника t свойство AcuteAngled эквивалентно тому, что все три угла меньше π/2.
LaTeX
$$$t.AcuteAngled \iff (\angle t_0 t_1 t_2 < \tfrac{\pi}{2}) \land (\angle t_1 t_2 t_0 < \tfrac{\pi}{2}) \land (\angle t_2 t_0 t_1 < \tfrac{\pi}{2})$$$
Lean4
theorem acuteAngled_iff_angle_lt {t : Triangle ℝ P} :
t.AcuteAngled ↔
∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2 :=
by
refine
⟨fun h ↦
⟨h _ _ _ (by decide) (by decide) (by decide), h _ _ _ (by decide) (by decide) (by decide),
h _ _ _ (by decide) (by decide) (by decide)⟩,
fun ⟨h012, h120, h201⟩ ↦ ?_⟩
have h210 := angle_comm (t.points 0) _ _ ▸ h012
have h021 := angle_comm (t.points 1) _ _ ▸ h120
have h102 := angle_comm (t.points 2) _ _ ▸ h201
intro i₁ i₂ i₃ h₁₂ h₁₃ h₂₃
fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp [*] at *
