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