norm_constOfIsEmpty — Mathlib

English

For an empty index set, the norm of a constant map equals the norm of the value.

Русский

Для пустого индекса норма константного отображения равна норме значения.

LaTeX

$$$\|\operatorname{constOfIsEmpty}_{\mathbb{K}}(E,\iota,F)(x)\| = \|x\|$$$

Lean4

@[simp]
theorem norm_constOfIsEmpty [IsEmpty ι] (x : F) : ‖constOfIsEmpty 𝕜 E ι x‖ = ‖x‖ :=
  ContinuousMultilinearMap.norm_constOfIsEmpty _ _ _

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