mul_angle_le_norm_sub — Mathlib

English

For unit vectors x,y, we have (2/π)·angle x y ≤ ‖x − y‖.

Русский

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

LaTeX

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

Lean4

/-- Chord-length is always greater than a multiple of arc-length. -/
theorem mul_angle_le_norm_sub (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : 2 / π * angle x y ≤ ‖x - y‖ :=
  (norm_sub_mem_Icc_angle hx hy).1

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