iIsOrtho — Mathlib

English

Define iIsOrtho B v to mean that the family v is orthogonal with respect to B, i.e., all pairwise B(v_i, v_j) = 0 for i ≠ j.

Русский

Определим iIsOrtho B v как семейство векторов, попарно ортогональное по отношению к B: для i ≠ j выполняется B(v_i, v_j) = 0.

LaTeX

$$$ \\mathrm{B}.iIsOrtho\\; v := B.IsOrthoᵢ v$$$

Lean4

/-- A set of vectors `v` is orthogonal with respect to some bilinear form `B` if and only
if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two elements, use
`BilinForm.IsOrtho` -/
def iIsOrtho {n : Type w} (B : BilinForm R M) (v : n → M) : Prop :=
  B.IsOrthoᵢ v

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