inner_finsupp_eq_zero — Mathlib

English

A linear combination supported on a set s that excludes index i is orthogonal to v_i: ⟪Finsupp.linearCombination 𝕜 v l, v i⟫ = 0 when i ∉ s.

Русский

Линейная комбинация, оперирующая над множеством s, не содержащим i, ортогональна v_i: ⟪Finsupp.linearCombination 𝕜 v l, v i⟫ = 0, если i ∉ s.

LaTeX

$$$i \notin s \Rightarrow \langle Finsupp.linearCombination 𝕜 v l, v i \rangle = 0$$$

Lean4

/-- A linear combination of some subset of an orthonormal set is orthogonal to other members of the
set. -/
theorem inner_finsupp_eq_zero {v : ι → E} (hv : Orthonormal 𝕜 v) {s : Set ι} {i : ι} (hi : i ∉ s) {l : ι →₀ 𝕜}
    (hl : l ∈ Finsupp.supported 𝕜 𝕜 s) : ⟪Finsupp.linearCombination 𝕜 v l, v i⟫ = 0 :=
  by
  rw [Finsupp.mem_supported'] at hl
  simp only [hv.inner_left_finsupp, hl i hi, map_zero]

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