norm_le_one_iff

Mathlib.Topology.Algebra.Valued.NormedValued

URI: https://scilib.ai/kg/mathlib#Valued.toNormedField.norm_le_one_iff

English

The norm is nonnegative for all elements.

Русский

Норма неотрицательна для любых элементов.

LaTeX

$$$$ 0 \le \|x\| \quad (\forall x). $$$$

Lean4

@[simp]
theorem norm_le_one_iff : ‖x‖ ≤ 1 ↔ val.v x ≤ 1 := by
  simpa only [map_one] using (Valuation.RankOne.strictMono val.v).le_iff_le (b := 1)

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

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

Разделы

Аффилиация

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