English
Existence of minimizers: for a nonempty complete convex subset K of a real inner product space and a vector u, there exists v ∈ K minimizing the distance to u.
Русский
Существование минимайзеров: для ненулевого полного выпуклого подмножества K в вещественном пространстве с внутренним произведением и вектора u существует элемент v ∈ K минимизирующий расстояние до u.
LaTeX
$$$\\exists v \\in K, \\|u-v\\| = \\inf_{w\\in K} \\|u-w\\|$$$
Lean4
/-- An orthonormal set in a finite-dimensional `InnerProductSpace` is maximal, if and only if it
is a basis. -/
theorem maximal_orthonormal_iff_basis_of_finiteDimensional (hv : Orthonormal 𝕜 ((↑) : v → E)) :
(∀ u ⊇ v, Orthonormal 𝕜 ((↑) : u → E) → u = v) ↔ ∃ b : Basis v 𝕜 E, ⇑b = ((↑) : v → E) :=
by
haveI := FiniteDimensional.proper_rclike 𝕜 (span 𝕜 v)
rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hv]
rw [Submodule.orthogonal_eq_bot_iff]
have hv_coe : range ((↑) : v → E) = v := by simp
constructor
· refine fun h => ⟨Basis.mk hv.linearIndependent _, Basis.coe_mk _ ?_⟩
convert h.ge
· rintro ⟨h, coe_h⟩
rw [← h.span_eq, coe_h, hv_coe]
