exists_not_self_orthogonal — Mathlib

English

For every projective point v, there exists some w such that v is not orthogonal to w.

Русский

Для каждой точки в проективном пространстве найдется такая другая точка w, для которой не выполняется ортогональность между ними.

LaTeX

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

Lean4

theorem exists_not_self_orthogonal (v : ℙ F (m → F)) : ∃ w, ¬orthogonal v w := by
  induction v with
  | h v hv =>
    rw [ne_eq, ← dotProduct_eq_zero_iff, not_forall] at hv
    obtain ⟨w, hw⟩ := hv
    exact ⟨mk F w fun h ↦ hw (by rw [h, dotProduct_zero]), hw⟩

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