English
A subfamily of an orthonormal family obtained by composing with an injective map is orthonormal.
Русский
Подсемейство ортонормированного набора, полученное композицией с инъективным отображением, остаётся ортонормированным.
LaTeX
$$$\operatorname{Orthonormal} 𝕜 v \rightarrow \forall f, \text{Injective } f \Rightarrow \operatorname{Orthonormal} 𝕜 (v \circ f)$$$
Lean4
/-- A subfamily of an orthonormal family (i.e., a composition with an injective map) is an
orthonormal family. -/
theorem comp {ι' : Type*} {v : ι → E} (hv : Orthonormal 𝕜 v) (f : ι' → ι) (hf : Function.Injective f) :
Orthonormal 𝕜 (v ∘ f) := by
classical
rw [orthonormal_iff_ite] at hv ⊢
intro i j
convert hv (f i) (f j) using 1
simp [hf.eq_iff]
