opNorm_subsingleton

Mathlib.Analysis.Normed.Operator.Basic

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

English

If the domain is a subsingleton (only one element), then every operator has norm zero.

Русский

Если область является одноэлементным, то у каждого оператора норма равна нулю.

LaTeX

$$$ \|f\| = 0 \quad\text{если } E \text{ subsingleton}$$$

Lean4

@[simp, nontriviality]
theorem opNorm_subsingleton [Subsingleton E] : ‖f‖ = 0 :=
  norm_of_subsingleton f

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

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

Разделы

Аффилиация

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