orthogonal_comm — Mathlib

English

Orthogonality is symmetric: for projective points v and w, orthogonal(v,w) holds iff orthogonal(w,v) holds.

Русский

Ортогональность симметрична: ортогональность(v,w) эквивалентна ортогональности(w,v).

LaTeX

$$$\\operatorname{orthogonal}(v,w) \\iff \\operatorname{orthogonal}(w,v)$$$

Lean4

theorem orthogonal_comm {v w : ℙ F (m → F)} : orthogonal v w ↔ orthogonal w v := by
  induction v with
  | h v hv =>
    induction w with
    | h w hw => rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]

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