one_lt_norm_iff

Mathlib.Topology.Algebra.Valued.NormedValued

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

English

Under the same setup, 1 < ‖x‖ if and only if 1 < v(x) for all x in L.

Русский

В той же конфигурации 1 < ‖x‖ эквивалентно 1 < v(x) для всех x ∈ L.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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