enorm_coe — Mathlib

English

The ENorm (extended norm) on Completion E satisfies the corresponding equality with the original ENorm on E for embedded elements.

Русский

ENorm на Completion E удовлетворяет тождеству для встроенных элементов по аналогии с ENorm на E.

LaTeX

$$$\|\,(x : Completion E)\|_{e} = \|x\|_{e}$$$

Lean4

@[simp]
theorem enorm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖ₑ = ‖x‖ₑ := by simp [enorm]

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