exists_not_orthogonal_self — Mathlib

English

There exists a w such that w is not orthogonal to v, for any v in projective space.

Русский

Существует такая точка w, что w не ортогональна v для любой заданной v в проективном пространстве.

LaTeX

$$$\\exists w:\\; \\lnot\\operatorname{orthogonal}(w,v)$$$

Lean4

theorem exists_not_orthogonal_self (v : ℙ F (m → F)) : ∃ w, ¬orthogonal w v :=
  by
  simp only [orthogonal_comm]
  exact exists_not_self_orthogonal v

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