oangle_sub_right_smul_rotation_pi_div_two

English

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

Русский

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

LaTeX

$$$ o.oangle\left(r\cdot rotation\left(\frac{\pi}{2}\right)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_right_smul_rotation_pi_div_two {x : V} (h : x ≠ 0) (r : ℝ) :
    o.oangle (r • o.rotation (π / 2 : ℝ) 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, hx, o.oangle_add_right_smul_rotation_pi_div_two]
  simpa [hr] using h

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