enorm_toContinuousLinearMap

Mathlib.Analysis.Normed.Operator.NormedSpace

URI: https://scilib.ai/kg/mathlib#LinearIsometry.enorm_toContinuousLinearMap

← MathLib Explorer

English

If f is a linear isometry, the operator norm of its toContinuousLinearMap equals 1.

Русский

Если f — линейная изометрия, то норма оператора равна 1.

LaTeX

$$$\\|f^{\\toContinuousLinearMap}\\| = 1$.$$

Lean4

@[simp]
theorem enorm_toContinuousLinearMap [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :
    ‖f.toContinuousLinearMap‖ₑ = 1 :=
  congrArg _ f.nnnorm_toContinuousLinearMap

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru