map_lt_map_iff

Mathlib.Algebra.Order.AbsoluteValue.Euclidean

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.IsEuclidean.map_lt_map_iff

English

For an IsEuclidean abv, abv x < abv y iff x ≺ y in the domain.

Русский

Для изометрически евклидова abv выполнено: abv x < abv y эквивалентно x ≺ y в исходном домене.

LaTeX

$$abv x < abv y \iff x \prec y$$

Lean4

theorem map_lt_map_iff {x y : R} (h : abv.IsEuclidean) : abv x < abv y ↔ x ≺ y :=
  map_lt_map_iff' h

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

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

Разделы

Аффилиация

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