opNNNorm_subsingleton

Mathlib.Analysis.Normed.Operator.NNNorm

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.opNNNorm_subsingleton

English

If the domain E is a subsingleton (has at most one element), then any operator has NNNorm 0.

Русский

Если область E — подсоединённое множество, тогда любой отображение имеет NNNorm 0.

LaTeX

$$$\\|f\\|_{+} = 0$ whenever $E$ is subsingleton$$

Lean4

@[simp, nontriviality]
theorem opNNNorm_subsingleton [Subsingleton E] (f : E →SL[σ₁₂] F) : ‖f‖₊ = 0 :=
  NNReal.eq <| f.opNorm_subsingleton

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

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

Разделы

Аффилиация

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