comp — Mathlib

English

If {V_i} is an orthogonal family and hv_family gives that each v_i is orthonormal, then the combined family a ↦ V_{a.1}(v_{a.1 a.2}) is orthonormal.

Русский

Если {V_i} образует ортогональную семью и hv_family задаёт, что каждый v_i - ортонормирован, то объединённая семействa a ↦ V_{a.1}(v_{a.1 a.2}) также ортонормирована.

LaTeX

$$$\\text{Orthonormal}_{\\mathbb{k}}\\, a \\mapsto V_{a.1}(v_{a.1 a.2})$$$

Lean4

/-- The composition of an orthogonal family of subspaces with an injective function is also an
orthogonal family. -/
theorem comp {γ : Type*} {f : γ → ι} (hf : Function.Injective f) :
    OrthogonalFamily 𝕜 (fun g => G (f g)) fun g => V (f g) := fun _i _j hij v w => hV (hf.ne hij) v w

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