inner_single_right — Mathlib

English

The norm defined by the product norm is preserved under the product equivalence: ‖equiv x‖ ≤ ‖x‖.

Русский

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

LaTeX

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

Lean4

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

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