enorm_enorm — Mathlib

English

In general, for ENorm spaces, the enorm applied to a norm of an element returns the same as the norm itself.

Русский

В общем виде для ENorm-пространств применение enorm к норме элемента возвращает ту же величину, что и норма элемента.

LaTeX

$$$\displaystyle \|\|x\|_e\|_e = \|x\|_e$$$

Lean4

theorem enorm_enorm {ε : Type*} [ENorm ε] (x : ε) : ‖‖x‖ₑ‖ₑ = ‖x‖ₑ := by simp [enorm]

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