isNonarchimedean_norm

Mathlib.Topology.Algebra.Valued.NormedValued

URI: https://scilib.ai/kg/mathlib#Valued.isNonarchimedean_norm

English

The norm is non-Archimedean, i.e., satisfies the strong triangle inequality.

Русский

Норма не-Архимедова: выполняется суровое неравенство по треугольнику.

LaTeX

$$$$ \text{Valued is nonarchimedean: } \|x+y\| \le \max(\|x\|, \|y\|). $$$$

Lean4

protected theorem isNonarchimedean_norm : IsNonarchimedean ((‖·‖) : L → ℝ) :=
  Valued.norm_add_le

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

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

Разделы

Аффилиация

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