isOrthoᵢ_def — Mathlib

English

The predicate IsOrthoᵢ(B, v) is defined by the condition that B(v_i, v_j) = 0 for all i ≠ j.

Русский

Предикат IsOrthoᵢ(B, v) определяется условием, что B(v_i, v_j) = 0 для всех i ≠ j.

LaTeX

$$$B.IsOrtho_i(v) \\iff \\forall i,j : n, \\ i \\neq j \\Rightarrow B(v_i, v_j) = 0$$$

Lean4

theorem isOrthoᵢ_def {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M} {v : n → M₁} :
    B.IsOrthoᵢ v ↔ ∀ i j : n, i ≠ j → B (v i) (v j) = 0 :=
  Iff.rfl

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