one_le_norm_iff

Mathlib.Topology.Algebra.Valued.NormedValued

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

English

Let L be as above. Then 1 ≤ ‖x‖ if and only if 1 ≤ v(x) for every x ∈ L.

Русский

Пусть L — указанное поле. Тогда 1 ≤ ‖x‖ эквивалентно 1 ≤ v(x) для каждого x ∈ L.

LaTeX

$$$1 \le \|x\| \iff 1 \le v(x)$$$

Lean4

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

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

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

Разделы

Аффилиация

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