nnnorm_changeOriginSeriesTerm — Mathlib

English

The NN norm of changeOriginSeriesTerm equals the NN norm of p(k+l).

Русский

NN-норма changeOriginSeriesTerm равна NN-норме p(k+l).

LaTeX

$$‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p(k+l)‖₊$$

Lean4

@[simp]
theorem nnnorm_changeOriginSeriesTerm (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
    ‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊ := by
  simp only [changeOriginSeriesTerm, LinearIsometryEquiv.nnnorm_map]

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