untrop_injective

Mathlib.Algebra.Tropical.Basic

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

English

The inverse (untrop) of tropicalization is injective as a map Tropical R → R.

Русский

Обратное отображение untrop тропикации Tropical R → R инъективно.

LaTeX

$$$\\mathrm{untrop}: \\mathrm{Tropical}\\,R \\to R \\text{ is injective}$$$

Lean4

theorem untrop_injective : Function.Injective (untrop : Tropical R → R) := fun _ _ => id

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

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

Разделы

Аффилиация

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