nnnorm_single — Mathlib

English

For DecidableEq ι and NormedAddCommGroup structure on each G_i, the NN-norm of the Pi.single i y equals the NN-norm of y.

Русский

При наличии структуры NormedAddCommGroup на каждом G_i и DecidableEq ι, NN-норма Pi.single i y равна NN-норме y.

LaTeX

$$$\|\Pi\!\text{single}_{i} (y)\|_+ = \|y\|_+$$$

Lean4

theorem nnnorm_single [DecidableEq ι] [∀ i, NormedAddCommGroup (G i)] {i : ι} (y : G i) : ‖Pi.single i y‖₊ = ‖y‖₊ :=
  by
  have H : ∀ b, ‖single i y b‖₊ = single (M := fun _ ↦ ℝ≥0) i ‖y‖₊ b :=
    by
    intro b
    refine Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b
    simp
  simp [Pi.nnnorm_def, H, Pi.single_apply, Finset.sup_ite, Finset.filter_eq']

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