opNorm_neg

Mathlib.Analysis.Normed.Group.Hom

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

English

The operator norm is invariant under negation: ‖-f‖ = ‖f‖.

Русский

Нормa оператора не изменяется при взятии отрицания: ‖-f‖ = ‖f‖.

LaTeX

$$$$ \| -f \| = \| f \| $$$$

Lean4

theorem opNorm_neg (f : NormedAddGroupHom V₁ V₂) : ‖-f‖ = ‖f‖ := by
  simp only [norm_def, coe_neg, norm_neg, Pi.neg_apply]

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

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

Разделы

Аффилиация

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