one_lt_iff

Mathlib.Analysis.AbsoluteValue.Equivalence

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.IsEquiv.one_lt_iff

English

Under isomorphism of absolute values, 1 < v x iff 1 < w x.

Русский

При изоморфизме абсолютных значений, 1 < v x эквивалентно 1 < w x.

LaTeX

$$$\\forall x, 1 < v x \\iff 1 < w x$ given IsEquiv between v and w$$

Lean4

theorem one_lt_iff (h : v.IsEquiv w) {x : R} : 1 < v x ↔ 1 < w x := by simpa only [map_one] using h.lt_iff_lt (x := 1)

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

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

Разделы

Аффилиация

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