orthogonal_top_eq_bot — Mathlib

English

Let B be a reflexive, nondegenerate bilinear form on a module M. Then the orthogonal of the whole space is {0}, i.e., every vector is orthogonal to all vectors only if it is zero.

Русский

Пусть B — это рефлексивная безнулевая билинейная форма на модуле M. Тогда ортогональность всей пространства равна нулю: любой вектор, ортогональный ко всем вектором, является нулевым.

LaTeX

$$$B.orthogonal(\top) = \bot$$$

Lean4

theorem orthogonal_top_eq_bot (hB : B.Nondegenerate) (hB₀ : B.IsRefl) : B.orthogonal ⊤ = ⊥ :=
  (Submodule.eq_bot_iff _).mpr fun _ hx ↦ hB _ fun y ↦ hB₀ _ _ <| hx y Submodule.mem_top

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