opNorm_nonneg

Mathlib.Analysis.NormedSpace.Multilinear.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMultilinearMap.opNorm_nonneg

English

The operator norm is always nonnegative: ∥f∥ ≥ 0.

Русский

Операторная норма всегда неотрицательна: ∥f∥ ≥ 0.

LaTeX

$$$$0 \\le \\|f\\|.$$$$

Lean4

theorem opNorm_nonneg (f : ContinuousMultilinearMap 𝕜 E G) : 0 ≤ ‖f‖ :=
  Real.sInf_nonneg fun _ ⟨hx, _⟩ => hx

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

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

Разделы

Аффилиация

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