inner_single_left — Mathlib

English

The norm of the image of x under the canonical equivalence is bounded by the product-norm of x: ‖equiv x‖ ≤ ‖x‖.

Русский

Норма образа x под каноническим эквивалентом ограничена нормой x на произведение: ‖equiv x‖ ≤ ‖x‖.

LaTeX

$$$\\|\\mathrm{equiv}\\;x\\| \\le \\|x\\|$$$

Lean4

@[simp]
theorem inner_single_left [DecidableEq ι] (x : C⋆ᵐᵒᵈ(A, Π i, E i)) {i : ι} (y : E i) :
    ⟪equiv _ _ |>.symm <| Pi.single i y, x⟫_A = ⟪y, x i⟫_A :=
  by
  simp only [pi_inner, equiv_symm_pi_apply]
  rw [Finset.sum_eq_single i]
  all_goals simp_all

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