opNorm_neg

Mathlib.Analysis.Normed.Operator.Basic

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

English

For any M ≥ 0, ‖f‖ ≤ M if and only if ∥f x∥ ≤ M ∥x∥ for all x.

Русский

Для любого M ≥ 0 выполняется: ‖f‖ ≤ M тогда и только тогда, когда ∥f x∥ ≤ M ∥x∥ для всех x.

LaTeX

$$$\\|f\\| \\le M \\iff \\forall x, \\|f x\\| \\le M \\|x\\| \\quad (M \\ge 0)$$$

Lean4

theorem opNorm_neg (f : E →SL[σ₁₂] F) : ‖-f‖ = ‖f‖ := by simp only [norm_def, neg_apply, norm_neg]

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

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

Разделы

Аффилиация

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