trop_monotone

Mathlib.Algebra.Tropical.Basic

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

English

The map trop: R → Tropical R is monotone with respect to the preorder on R.

Русский

Отображение trop уведено монотонно относительно порядка на R.

LaTeX

$$$\\forall x,y\\in R,\\; x \\le y \\Rightarrow \\operatorname{trop}(x) \\le \\operatorname{trop}(y)$$$

Lean4

theorem trop_monotone [Preorder R] : Monotone (trop : R → Tropical R) := fun _ _ => id

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

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

Разделы

Аффилиация

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