codRestrict — Mathlib

English

If a family is orthonormal and each vector lies in a subspace, then restricting to that subspace preserves orthonormality.

Русский

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

LaTeX

$$Orthonormal v → s and hv: orthonormal on Set.codRestrict v s hv$$

Lean4

theorem codRestrict {ι : Type*} {v : ι → E} (hv : Orthonormal 𝕜 v) (s : Submodule 𝕜 E) (hvs : ∀ i, v i ∈ s) :
    @Orthonormal 𝕜 s _ _ _ ι (Set.codRestrict v s hvs) :=
  s.subtypeₗᵢ.orthonormal_comp_iff.mp hv

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