𝕜 : Type u_1
E : Type u_2
F : Type ?u.2141610
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
s : Set ι
i : ι
hi : ¬i ∈ s
l : ι →₀ 𝕜
hl : ∀ (x : ι), ¬x ∈ s → ↑l x = 0
⊢ inner (↑(Finsupp.total ι E 𝕜 v) l) (v i) = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2141610
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
s : Set ι
i : ι
hi : ¬i ∈ s
l : ι →₀ 𝕜
hl : l ∈ Finsupp.supported 𝕜 𝕜 s
⊢ inner (↑(Finsupp.total ι E 𝕜 v) l) (v i) = 0
rw [Finsupp.mem_supported'] at hl
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2141610
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
s : Set ι
i : ι
hi : ¬i ∈ s
l : ι →₀ 𝕜
hl : ∀ (x : ι), ¬x ∈ s → ↑l x = 0
⊢ inner (↑(Finsupp.total ι E 𝕜 v) l) (v i) = 0
simp only [hv.inner_left_finsupp, hl i hi, map_zero]