norm_constOfIsEmpty — Mathlib

English

When the index set is empty, the norm of the constant map built from an element x in G is exactly the norm of x. This reflects that there is no multilinear interaction to bound beyond the constant map.

Русский

Если множество индексов пусто, норма константного отображения, заданного элементом x в G, равна норме x.

LaTeX

$$$\|\mathrm{constOfIsEmpty}_{\mathbb{K}}(E,x)\| = \|x\|$$$

Lean4

@[simp]
theorem norm_constOfIsEmpty [IsEmpty ι] (x : G) : ‖constOfIsEmpty 𝕜 E x‖ = ‖x‖ :=
  by
  apply le_antisymm
  · refine opNorm_le_bound (norm_nonneg _) fun x => ?_
    rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]
  · simpa using (constOfIsEmpty 𝕜 E x).le_opNorm 0

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