norm_apply_le_norm — Mathlib

English

For each i, the component norm is bounded by the norm of the whole x: ‖x_i‖ ≤ ‖x‖.

Русский

Для каждого i нормa компонента не превышает норму всего x: ‖x_i‖ ≤ ‖x‖.

LaTeX

$$$\\|x_i\\| \\le \\|x\\|$ for all i$$

Lean4

theorem norm_apply_le_norm (x : C⋆ᵐᵒᵈ(A, Π i, E i)) (i : ι) : ‖x i‖ ≤ ‖x‖ :=
  by
  let _ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, Π i, E i) := normedAddCommGroup A
  refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2
  rw [pi_norm_sq, norm_sq_eq A]
  refine CStarAlgebra.norm_le_norm_of_nonneg_of_le inner_self_nonneg ?_
  exact Finset.single_le_sum (fun j _ ↦ inner_self_nonneg (A := A) (x := x j)) (Finset.mem_univ i)

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