nnnorm_toContinuousLinearMap

Mathlib.Analysis.Normed.Operator.NormedSpace

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

← MathLib Explorer

English

The nnreal norm of the identity map equals 1.

Русский

nnnorm идентичности равна 1.

LaTeX

$$$\\|\\mathrm{id}\\|_{nn} = 1.$$$

Lean4

@[simp]
theorem nnnorm_toContinuousLinearMap [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :
    ‖f.toContinuousLinearMap‖₊ = 1 :=
  Subtype.ext f.norm_toContinuousLinearMap

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

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

Разделы

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

Аффилиация

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