nnnorm_constOfIsEmpty — Mathlib

English

In the empty-index case, the NN-norm of the constant map equals the NN-norm of x, mirroring the previous norm equality in NN-real terms.

Русский

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

LaTeX

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

Lean4

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

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