nnnorm_add_one_le_max_nnnorm_one

Mathlib.Analysis.Normed.Ring.Ultra

URI: https://scilib.ai/kg/mathlib#IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one

English

With the NNReal norm in an ultrametric setting, we have ‖x+1‖₊ ≤ max(‖x‖₊,1).

Русский

В ультраметрическом окружении с NNNorm выполняется ‖x+1‖₊ ≤ max(‖x‖₊,1).

LaTeX

$$$\|x+1\|_{+} \le \max\{\|x\|_{+}, 1\}$$$

Lean4

theorem nnnorm_add_one_le_max_nnnorm_one (x : R) : ‖x + 1‖₊ ≤ max ‖x‖₊ 1 :=
  norm_add_one_le_max_norm_one _

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

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

Разделы

Аффилиация

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