enorm_map — Mathlib

English

Let f be a semilinear isometry. Then for every x, the ENNorm of f(x) equals the ENNorm of x.

Русский

Пусть f является полу-линейной изометрией. Тогда для любого x имеет место равенство ENNorm: ‖f(x)‖ₑ = ‖x‖ₑ.

LaTeX

$$$‖f(x)‖_e = ‖x‖_e$$$

Lean4

@[simp]
  -- Should be replaced with `SemilinearIsometryClass.enorm_map` when https://github.com/leanprover/lean4/issues/3107 is fixed.

theorem enorm_map (x : E) : ‖f x‖ₑ = ‖x‖ₑ := by simp [enorm]

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