isOrthoᵢ_flip — Mathlib

English

The orthogonality of a family with respect to B is equivalent to its orthogonality with respect to the flipped form B, i.e., IsOrthoᵢ(B, v) ⇔ IsOrthoᵢ(B.flip, v).

Русский

Ортогональность семейства относительно B эквивалентна ортогональности относительно переставленной формы B, то есть IsOrthoᵢ(B, v) ⇔ IsOrthoᵢ(B.flip, v).

LaTeX

$$$B.IsOrtho_i(v) \\iff (B.flip).IsOrtho_i(v)$$$

Lean4

theorem isOrthoᵢ_flip (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M) {v : n → M₁} : B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v :=
  by
  simp_rw [isOrthoᵢ_def]
  constructor <;> exact fun h i j hij ↦ h j i hij.symm

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