norm_single — Mathlib

English

The norm of the image of a single coordinate y in E_i under the canonical equivalence is ‖y‖.

Русский

Норма образа единичного координатного элемента y в E_i через каноническое соответствие равна ‖y‖.

LaTeX

$$$\\|\\mathrm{equiv}\\;|\\!\\!\u2060\\!\\! (Pi.single\\ i\\ y)\\| = \\|y\\|$$$

Lean4

@[simp]
theorem norm_single [DecidableEq ι] (i : ι) (y : E i) : ‖equiv A _ |>.symm <| Pi.single i y‖ = ‖y‖ :=
  by
  let _ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, Π i, E i) := normedAddCommGroup A
  rw [← sq_eq_sq₀ (by positivity) (by positivity)]
  simp [norm_sq_eq A]

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