orthonormal_subtype_range — Mathlib

English

An injective v yields equivalence of orthonormality between v and the subtype val.

Русский

Инъективное отображение v сохраняет ортонормированность между v и базисом подтипа.

LaTeX

$$$\operatorname{Orthonormal} 𝕜 (v) \iff \operatorname{Orthonormal} 𝕜 (\operatorname{Subtype.val})$$$

Lean4

/-- An injective family `v : ι → E` is orthonormal if and only if `Subtype.val : (range v) → E` is
orthonormal. -/
theorem orthonormal_subtype_range {v : ι → E} (hv : Function.Injective v) :
    Orthonormal 𝕜 (Subtype.val : Set.range v → E) ↔ Orthonormal 𝕜 v :=
  by
  let f : ι ≃ Set.range v := Equiv.ofInjective v hv
  refine ⟨fun h => h.comp f f.injective, fun h => ?_⟩
  rw [← Equiv.self_comp_ofInjective_symm hv]
  exact h.comp f.symm f.symm.injective

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