gramSchmidt_pairwise_orthogonal — Mathlib

English

The Gram-Schmidt family is pairwise orthogonal: for any a ≠ b, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0.

Русский

Семейство Грамма-Шмидта попарно ортогонально: для любых a ≠ b выполняется ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0.

LaTeX

$$$ \text{Pairwise } \langle \mathrm{gramSchmidt}_{\mathbb{K}}(f)(a), \mathrm{gramSchmidt}_{\mathbb{K}}(f)(b) \rangle = 0 \quad (a \neq b)$$$

Lean4

/-- This is another version of `gramSchmidt_orthogonal` using `Pairwise` instead. -/
theorem gramSchmidt_pairwise_orthogonal (f : ι → E) : Pairwise fun a b => ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0 :=
  fun _ _ => gramSchmidt_orthogonal 𝕜 f

Похожие утверждения