English
Let B be a sesquilinear form on a vector space M and v: n → M. Then the family v is orthogonal with respect to B if and only if B(v_i, v_j) = 0 for all i ≠ j.
Русский
Пусть B — сескалиентная форма на векторном пространстве M, а v : n → M. Тогда множество v ортогонально относительно B тогда и только тогда, когда для всех i ≠ j выполняется B(v_i, v_j) = 0.
LaTeX
$$$\\mathrm{IsOrth}_B(v) \\;\\Longleftrightarrow\\; \\forall i\\,j \\in n,\\ i \\neq j \\Rightarrow B(v_i, v_j) = 0$$$
Lean4
/-- A set of vectors `v` is orthogonal with respect to some bilinear map `B` if and only
if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two elements, use
`BilinForm.isOrtho` -/
def IsOrthoᵢ (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M) (v : n → M₁) : Prop :=
Pairwise (B.IsOrtho on v)
