neg_iff

Mathlib.Analysis.Normed.Group.Hom

URI: https://scilib.ai/kg/mathlib#NormedAddGroupHom.NormNoninc.neg_iff

← MathLib Explorer

English

For any f, (−f).NormNoninc is equivalent to f.NormNoninc.

Русский

Для любого f, (−f).NormNoninc эквивалентно f.NormNoninc.

LaTeX

$$$(-f).NormNoninc \\iff f.NormNoninc$$$

Lean4

@[simp]
theorem neg_iff {f : NormedAddGroupHom V₁ V₂} : (-f).NormNoninc ↔ f.NormNoninc :=
  ⟨fun h x => by simpa using h x, fun h x => (norm_neg (f x)).le.trans (h x)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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