coe_normSeminorm — Mathlib

English

The canonical embedding (coercion) of normSeminorm into functions coincides with the usual norm: for all x, (normSeminorm 𝕜 E)(x) = ||x||.

Русский

Единая индукция нормальной семинормы в функцию совпадает с обычной нормой: для всех x выполняется (normSeminorm 𝕜 E)(x) = ||x||.

LaTeX

$$$\forall x, (\text{normSeminorm } 𝕜 E)(x) = \|x\|.$$$

Lean4

@[simp]
theorem coe_normSeminorm : ⇑(normSeminorm 𝕜 E) = norm :=
  rfl

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