map_sub_le_max

Mathlib.Analysis.Normed.Group.Seminorm

URI: https://scilib.ai/kg/mathlib#map_sub_le_max

← MathLib Explorer

English

For a nonarchimedean seminorm class, f(x − y) ≤ max(f(x), f(y)).

Русский

Для неархиморова неаналитного класса нормала выполняется f(x − y) ≤ max(f(x), f(y)).

LaTeX

$$f(x - y) \\le \\max(f(x), f(y))$$

Lean4

theorem map_sub_le_max : f (x - y) ≤ max (f x) (f y) :=
  by
  rw [sub_eq_add_neg, ← NonarchAddGroupSeminormClass.map_neg_eq_map' f y]
  exact map_add_le_max _ _ _

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

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

Разделы

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

Аффилиация

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