rightInverse_trop

Mathlib.Algebra.Tropical.Basic

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

English

The tropicalization map trop has a right inverse given by untrop: trop(untrop(y)) = y.

Русский

У trop есть правый обратный, заданный untrop: trop(untrop(y)) = y.

LaTeX

$$$\\mathrm{RightInverse}\\ (\\mathrm{trop})\\ (\\mathrm{untrop})$$$

Lean4

theorem rightInverse_trop : Function.RightInverse (trop : R → Tropical R) untrop :=
  untrop_trop

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

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

Разделы

Аффилиация

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