oangle_sub_left_smul_rotation_pi_div_two

English

For x and r, o.oangle(x − r·rotation(π/2)x, x) equals arctan r.

Русский

Угол между x−r·rotation(π/2)x и x равен arctan r.

LaTeX

$$$ o.oangle\left(x - r\cdot rotation\left(\frac{\pi}{2}\right)x, x\right) = \arctan r $$$

Lean4

/-- An angle in a right-angled triangle expressed using `arctan`, where one side is a multiple
of a rotation of another by `π / 2`, version subtracting vectors. -/
theorem oangle_sub_left_smul_rotation_pi_div_two {x : V} (h : x ≠ 0) (r : ℝ) :
    o.oangle (x - r • o.rotation (π / 2 : ℝ) x) x = Real.arctan r :=
  by
  by_cases hr : r = 0; · simp [hr]
  have hx : x = r⁻¹ • o.rotation (π / 2 : ℝ) (-(r • o.rotation (π / 2 : ℝ) x)) := by simp [hr, ← Real.Angle.coe_add]
  rw [sub_eq_add_neg, add_comm]
  nth_rw 3 [hx]
  nth_rw 2 [hx]
  rw [o.oangle_add_left_smul_rotation_pi_div_two, inv_inv]
  simpa [hr] using h

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