English
Let S be an orthonormal set in E, considered as a subset of E via a subtype. Then there exists a maximal extension within subtypes, containing S, and maximal with respect to inclusion among orthonormal subtype-extensions.
Русский
Пусть S — ортонормированная совокупность в E, рассматриваемая как подмножество через подтип. Тогда существует максимальное продолжение внутри подтипов, содержащее S и максимальное по включению среди ортонормированных продолжений в подтипе.
LaTeX
$$$\\exists W\\supseteq S\\,\\bigl(\\operatorname{Orthonormal}_{\\mathbb{K}}(\\operatorname{Subtype.val}:W\\to E)\\ \\wedge\\ \\forall U\\supseteq W,\\ \\operatorname{Orthonormal}_{\\mathbb{K}}(\\operatorname{Subtype.val}:U\\to E)\\to U=W\\bigr).$$$
Lean4
/-- A linear isometry preserves the property of being orthonormal. -/
theorem orthonormal_comp_iff {v : ι → E} (f : E →ₗᵢ[𝕜] E') : Orthonormal 𝕜 (f ∘ v) ↔ Orthonormal 𝕜 v := by
classical simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]
