English
Let E be a vector space over 𝕜 with an inner product, and let v ∈ E and a finite family vs = (vs_i) for i in {0,1,...,n−1}. The concatenation of v with vs, denoted vecCons(v, vs), is orthonormal if and only if v has unit length, is orthogonal to each vs_i, and the family vs is orthonormal; equivalently, Orthonormal 𝕜 (Matrix.vecCons v vs) ⇔ ∥v∥ = 1 ∧ (∀ i, ⟪v, vs_i⟫ = 0) ∧ Orthonormal 𝕜 vs.
Русский
Пусть E — пространство векторных величин над 𝕜 с правдоподобным скалярным произведением. Пусть v ∈ E и семейство vs = (vs_i) для i = 0,...,n−1. Объединение vecCons(v, vs) является ортонормированным набором тогда и только тогда, когда вектор v имеет норму 1, ортогонален каждому vs_i, и сам набор vs ортонормирован; то есть Orthonormal 𝕜 (Matrix.vecCons v vs) эквивалентно ∥v∥ = 1 и (∀ i, ⟪v, vs_i⟫ = 0) и Orthonormal 𝕜 vs.
LaTeX
$$$\operatorname{Orthonormal} 𝕜 (\mathrm{Matrix.vecCons}\ v\ vs) \iff \|v\| = 1 \wedge (\forall i, \langle v, vs\,i\rangle = 0) \wedge \operatorname{Orthonormal} 𝕜 vs$$$
Lean4
@[simp]
theorem orthonormal_vecCons_iff {n : ℕ} {v : E} {vs : Fin n → E} :
Orthonormal 𝕜 (Matrix.vecCons v vs) ↔ ‖v‖ = 1 ∧ (∀ i, ⟪v, vs i⟫ = 0) ∧ Orthonormal 𝕜 vs :=
by
simp_rw [Orthonormal, pairwise_fin_succ_iff_of_isSymm, Fin.forall_fin_succ]
tauto
