nnnorm_constOfIsEmpty — Mathlib

English

In the empty-index case, the NN-norm of constOfIsEmpty equals the NN-norm of the value.

Русский

В случае пустого индекса NN-норма константы равна NN-норме значения.

LaTeX

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

Lean4

@[simp]
theorem nnnorm_constOfIsEmpty [IsEmpty ι] (x : F) : ‖constOfIsEmpty 𝕜 E ι x‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_constOfIsEmpty _ _ _

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