inner_eq_zero_iff_angle_eq_pi_div_two

English

Two vectors are orthogonal if and only if their inner product is zero, which corresponds to the angle between them being π/2.

Русский

Две вектора ортогональны тогда и только тогда, когда их скалярное произведение равно нулю, что соответствует углу между ними равному π/2.

LaTeX

$$$⟪x, y⟫ = 0 \\\\Longleftrightarrow \\\\angle x y = \\\\pi/2$$$

Lean4

/-- Two vectors have inner product 0 if and only if the angle between
them is π/2. -/
theorem inner_eq_zero_iff_angle_eq_pi_div_two (x y : V) : ⟪x, y⟫ = 0 ↔ angle x y = π / 2 :=
  Iff.symm <| by simp +contextual [angle, or_imp]

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