angle_le_mul_norm_sub — Mathlib

English

For unit vectors x,y, the angle between them satisfies angle x y ≤ (π/2) · ‖x − y‖.

Русский

Для единичных векторов x,y угол между ними удовлетворяет: angle x y ≤ (π/2)·‖x − y‖.

LaTeX

$$$$\angle x y \le \frac{\pi}{2} \|x - y\|, \quad \|x\| = \|y\| = 1.$$$$

Lean4

/-- Arc-length is always less than a multiple of chord-length. -/
theorem angle_le_mul_norm_sub (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : angle x y ≤ π / 2 * ‖x - y‖ := by
  rw [← div_le_iff₀' <| by positivity, div_eq_inv_mul, inv_div]; exact mul_angle_le_norm_sub hx hy

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