linearIsometry_apply_single — Mathlib

English

For a dfinsupp W0, hV.linearIsometry(W0.sum(lp.single 2)) equals W0.sum(V_i).

Русский

Для dfinsupp W0, hV.linearIsometry(W0.sum(lp.single 2)) равно W0.sum(V_i).

LaTeX

$$$ hV.linearIsometry\\left(W_0.sum(\\text{lp.single } 2)\\right) = W_0.sum_i V_i $$$

Lean4

@[simp]
protected theorem linearIsometry_apply_single [DecidableEq ι] {i : ι} (x : G i) :
    hV.linearIsometry (lp.single 2 i x) = V i x :=
  by
  rw [hV.linearIsometry_apply, ← tsum_ite_eq i (V i x)]
  congr
  ext j
  rw [lp.single_apply]
  split_ifs with h
  · subst h; simp
  · simp [h]

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