norm_add_one_le_max_norm_one — Mathlib

English

In an ultrametric normed ring, for every x, the norm of x+1 is bounded by the maximum of the norm of x and 1: ||x+1|| ≤ max(||x||, 1).

Русский

В ультраметрическом нормированном кольце выполняется неравенство ||x+1|| ≤ max(||x||, 1) для всех x.

LaTeX

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

Lean4

theorem norm_add_one_le_max_norm_one (x : R) : ‖x + 1‖ ≤ max ‖x‖ 1 := by
  simpa only [le_max_iff, norm_one] using norm_add_le_max x 1

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