IsOrtho — Mathlib

English

Two elements x, y are orthogonal with respect to B if and only if B(x, y) = 0.

Русский

Два элемента x, y ортогональны относительно B тогда и только тогда, когда B(x, y) = 0.

LaTeX

$$$ B.IsOrtho(x,y) \\iff B(x,y) = 0 $$$

Lean4

/-- The proposition that two elements of a bilinear form space are orthogonal. For orthogonality
of an indexed set of elements, use `BilinForm.iIsOrtho`. -/
def IsOrtho (B : BilinForm R M) (x y : M) : Prop :=
  B x y = 0

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