English
If an orthonormal set on a subset has the correct cardinality, it can be extended to an orthonormal basis with the specified coordinates.
Русский
Если на подмножестве задан ортонормированный набор иCardinality совпадает, то его можно дополнить до ортонормированного базиса так, чтобы координаты совпадали с заданными.
LaTeX
$$Exists b : OrthonormalBasis ι 𝕜 E, ∀ i ∈ s, b i = v i$$
Lean4
theorem exists_orthonormalBasis_extension_of_card_eq {ι : Type*} [Fintype ι] (card_ι : finrank 𝕜 E = Fintype.card ι)
{v : ι → E} {s : Set ι} (hv : Orthonormal 𝕜 (s.restrict v)) : ∃ b : OrthonormalBasis ι 𝕜 E, ∀ i ∈ s, b i = v i :=
by
have hsv : Injective (s.restrict v) := hv.linearIndependent.injective
have hX : Orthonormal 𝕜 ((↑) : Set.range (s.restrict v) → E) := by rwa [orthonormal_subtype_range hsv]
obtain ⟨Y, b₀, hX, hb₀⟩ := hX.exists_orthonormalBasis_extension
have hιY : Fintype.card ι = Y.card := by
refine card_ι.symm.trans ?_
exact Module.finrank_eq_card_finset_basis b₀.toBasis
have hvsY : s.MapsTo v Y := (s.mapsTo_image v).mono_right (by rwa [← range_restrict])
have hsv' : Set.InjOn v s := by
rw [Set.injOn_iff_injective]
exact hsv
obtain ⟨g, hg⟩ := hvsY.exists_equiv_extend_of_card_eq hιY hsv'
use b₀.reindex g.symm
intro i hi
simp [hb₀, hg i hi]
