opNNNorm_mul

Mathlib.Analysis.Normed.Operator.Mul

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

English

The NNReal-norm of the left-multiplication operator by R is equal to 1; i.e., ‖mul 𝕜 R‖₊ = 1.

Русский

NNNorm левого умножения на R равен единице: ‖mul 𝕜 R‖₊ = 1.

LaTeX

$$$\\|\\mathrm{mul}_{\\mathbb{K},R}\\|_{+} = 1$$$

Lean4

@[simp]
theorem opNNNorm_mul : ‖mul 𝕜 R‖₊ = 1 :=
  Subtype.ext <| opNorm_mul 𝕜 R

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

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

Разделы

Аффилиация

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