untrop_monotone

Mathlib.Algebra.Tropical.Basic

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

English

The map untrop: Tropical R → R is monotone with respect to the tropical preorder.

Русский

Карта untrop: Tropical R → R монотонна относительно тропического порядка.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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