tropOrderIso

Mathlib.Algebra.Tropical.Basic

URI: https://scilib.ai/kg/mathlib#Tropical.tropOrderIso

← MathLib Explorer

English

There exists an order isomorphism between R and Tropical R, realized by tropOrderIso.

Русский

Существует сверхпорядковый изоморфизм между R и Tropical R, заданный tropOrderIso.

LaTeX

$$$R \\cong_o Tropical R$$$

Lean4

/-- Reinterpret `x : R` as an element of `Tropical R`, preserving the order. -/
def tropOrderIso [Preorder R] : R ≃o Tropical R :=
  { tropEquiv with map_rel_iff' := untrop_le_iff }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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