orthogonalFamily_iff_pairwise — Mathlib

English

Two submodules from an orthogonal family with different indices are orthogonal.

Русский

Два подмодуля из ортогонального семейства с различными индексами ортогональны друг другу.

LaTeX

$$isOrtho {ι} {V : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) {i j : ι} (hij : i ≠ j) : V_i ⟂ V_j$$

Lean4

theorem orthogonalFamily_iff_pairwise {ι} {V : ι → Submodule 𝕜 E} :
    (OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) ↔ Pairwise ((· ⟂ ·) on V) :=
  forall₃_congr fun _i _j _hij =>
    Subtype.forall.trans <|
      forall₂_congr fun _x _hx => Subtype.forall.trans <| forall₂_congr fun _y _hy => inner_eq_zero_symm

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