norm_single_le_one — Mathlib

English

For each i in a finite index set, the operator norm of the single projection map is at most 1: ||ContinuousLinearMap.single 𝕜 E i|| ≤ 1.

Русский

Для каждого i из конечного множества индексов норма оператора линейного отображения single не больше единицы: ||single_i|| ≤ 1.

LaTeX

$$$$\\|\\mathrm{single}_{\\mathbb{K}}(i)\\| \\le 1.$$$$

Lean4

theorem norm_single_le_one [∀ i, SeminormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (i : ι) :
    ‖ContinuousLinearMap.single 𝕜 E i‖ ≤ 1 :=
  (LinearIsometry.single 𝕜 E i).norm_toContinuousLinearMap_le

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