isOrtho — Mathlib

English

If a family is orthogonal, then any two distinct indices give orthogonal submodules.

Русский

Если семейство ортогонально, то для любых различных индексов подмодули ортогональны.

LaTeX

$$hV.pairwise hij$$

Lean4

/-- Two submodules in an orthogonal family with different indices are orthogonal. -/
theorem isOrtho {ι} {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) {i j : ι}
    (hij : i ≠ j) : V i ⟂ V j :=
  hV.pairwise hij

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